Quelle  ROOT

chapter AFP

session ML_Unification = HOL +
  description
    \<open>Various unification utilities for Isabelle/ML, e.g. proof-producing E-unification, E-matching, and unification hints.\<close>
  options [timeout = 300]
  sessions
    SpecCheck
  directories
    "Binders"
    "Examples"
    "Logger"
    "Logger/Data_Structures"
    "ML_Utils"
    "ML_Utils/Attributes"
    "ML_Utils/Conversions"
    "ML_Utils/Costs_Priorities"
    "ML_Utils/Functor_Instances"
    "ML_Utils/General"
    "ML_Utils/Generic_Data"
    "ML_Utils/Methods"
    "ML_Utils/ML_Attributes"
    "ML_Utils/ML_Code"
    "ML_Utils/Parsing"
    "ML_Utils/Tactics"
    "ML_Utils/Terms"
    "ML_Utils/Theorems"
    "Normalisations"
    "Simps_To"
    "Term_Index"
    "Tests"
    "Unifiers"
    "Unification_Attributes"
    "Unification_Hints"
    "Unification_Parsers"
    "Unification_Tactics"
    "Unification_Tactics/Assumption"
    "Unification_Tactics/Fact"
    "Unification_Tactics/Resolution"
  theories
    ML_Logger
    ML_Logger_Examples
    ML_Utils
    ML_Unifiers
    Unification_Tactics
    Unification_Attributes
    ML_Unification_Hints
    ML_Unification_HOL_Setup
    E_Unification_Examples
    Unification_Hints_Reification_Examples
  theories [document = false]
    ML_Unification_Tests
  document_files
    "root.tex"
    "root.bib"