Diffusion afp-devel a5d6a4c1351d

new entry ML_Unification
a5d6a4c1351d
Actions

Tags

None

Subscribers

None

Description

new entry ML_Unification

Details

Provenance

Authored on

Parents

rAFPa310c88be4ac: Inserted another missing acknowledgement

Branches

Unknown

Tags

Unknown

Event Timeline

traytel committed rAFPa5d6a4c1351d: new entry ML_Unification.Oct 4 2023, 5:27 PM

Changes (136)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

E_Unification_Examples.thy

Unification_Hints_Reification_Examples.thy

Data_Structures

binding_tree.ML

hoption_tree.ML

ML_Logger_Examples.thy

Setup_Result_Commands.thy

logging_antiquotation.ML

ML_Unification_Base.thy

ML_Unification_HOL_Setup.thy

ML_Attribute_Utils.thy

attribute_util.ML

ML_Conversion_Utils.thy

conversion_util.ML

Functor_Instances

ML_Functor_Instances.thy

functor_instance.ML

functor_instance_antiquot.ML

ML_General_Utils.thy

general_util.ML

ML_Generic_Data_Utils.thy

pair_generic_data_args.ML

ML_Attributes.thy

ml_attribute.ML

ML_Code_Utils.thy

ml_code_util.ML

ml_syntax_util.ML

ML_Method_Utils.thy

ML_Parsing_Utils.thy

parse_key_value.ML

parse_key_value_antiquot.ML

ML_Priorities.thy

ML_Tactic_Utils.thy

ML_Term_Utils.thy

ML_Theorem_Utils.thy

ML_Normalisations.thy

envir_normalisation.ML

term_normalisation.ML

simps_to_unif.ML

ML_Term_Index.thy

discrimination_tree.ML

term_index_data.ML

First_Order_ML_Unification_Tests.thy

Higher_Order_ML_Unification_Tests.thy

Higher_Order_Pattern_ML_Unification_Tests.thy

ML_Unification_Tests.thy

ML_Unification_Tests_Base.thy

first_order_unification_tests.ML

higher_order_pattern_unification_tests.ML

Unification_Attributes

Unification_Attributes.thy

unify_of_base.ML

Unification_Hints

ML_Unification_Hints.thy

named_theorems_unification_hints.ML

term_index_unification_hints.ML

unification_hints.ML

unification_hints_base.ML

Unification_Parsers

ML_Unification_Parsers.thy

unification_parser.ML

Unification_Tactics

Unify_Assumption_Tactic.thy

unify_assumption.ML

unify_assumption_base.ML

Unify_Fact_Tactic.thy

unify_fact_base.ML

Unify_Resolve_Tactics.thy

unify_resolve.ML

unify_resolve_base.ML

Unification_Tactics.thy

ML_Unifiers.thy

first_order_unification.ML

higher_order_pattern_unification.ML

higher_order_unification.ML

higher_ordern_pattern_first_decomp_unification.ML

mixed_unification.ML

simplifier_unification.ML

tactic_unification.ML

unification_combinator.ML

unification_combine.ML

unification_base.ML

unification_util.ML

rAFPa5d6a4c1351d

thys/ML_Unification/Binders/ML_Binders.thy

thys/ML_Unification/Binders/binders.ML

thys/ML_Unification/Examples/E_Unification_Examples.thy

thys/ML_Unification/Examples/Unification_Hints_Reification_Examples.thy

thys/ML_Unification/Logger/Data_Structures/binding_tree.ML

thys/ML_Unification/Logger/Data_Structures/hoption_tree.ML

thys/ML_Unification/Logger/Data_Structures/map.ML

thys/ML_Unification/Logger/ML_Logger.thy

thys/ML_Unification/Logger/ML_Logger_Examples.thy

thys/ML_Unification/Logger/README.md

thys/ML_Unification/Logger/Setup_Result_Commands.thy

thys/ML_Unification/Logger/logger.ML

thys/ML_Unification/Logger/logging_antiquotation.ML

thys/ML_Unification/ML_Unification_Base.thy

thys/ML_Unification/ML_Unification_HOL_Setup.thy

thys/ML_Unification/ML_Utils/Attributes/ML_Attribute_Utils.thy

thys/ML_Unification/ML_Utils/Attributes/attribute_util.ML

thys/ML_Unification/ML_Utils/Conversions/ML_Conversion_Utils.thy

thys/ML_Unification/ML_Utils/Conversions/conversion_util.ML

thys/ML_Unification/ML_Utils/Functor_Instances/ML_Functor_Instances.thy

thys/ML_Unification/ML_Utils/Functor_Instances/functor_instance.ML

thys/ML_Unification/ML_Utils/Functor_Instances/functor_instance_antiquot.ML

thys/ML_Unification/ML_Utils/General/ML_General_Utils.thy

thys/ML_Unification/ML_Utils/General/general_util.ML

thys/ML_Unification/ML_Utils/Generic_Data/ML_Generic_Data_Utils.thy

thys/ML_Unification/ML_Utils/Generic_Data/pair_generic_data_args.ML

thys/ML_Unification/ML_Utils/ML_Attributes/ML_Attributes.thy

thys/ML_Unification/ML_Utils/ML_Attributes/ml_attribute.ML

thys/ML_Unification/ML_Utils/ML_Code/ML_Code_Utils.thy

thys/ML_Unification/ML_Utils/ML_Code/ml_code_util.ML

thys/ML_Unification/ML_Utils/ML_Code/ml_syntax_util.ML

thys/ML_Unification/ML_Utils/ML_Utils.thy

thys/ML_Unification/ML_Utils/Methods/ML_Method_Utils.thy

thys/ML_Unification/ML_Utils/Methods/method_util.ML

thys/ML_Unification/ML_Utils/Parsing/ML_Parsing_Utils.thy

thys/ML_Unification/ML_Utils/Parsing/parse_key_value.ML

thys/ML_Unification/ML_Utils/Parsing/parse_key_value_antiquot.ML

thys/ML_Unification/ML_Utils/Parsing/parse_util.ML

thys/ML_Unification/ML_Utils/Priorities/ML_Priorities.thy

thys/ML_Unification/ML_Utils/Priorities/priority.ML

thys/ML_Unification/ML_Utils/Tactics/ML_Tactic_Utils.thy

thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML

thys/ML_Unification/ML_Utils/Terms/ML_Term_Utils.thy

thys/ML_Unification/ML_Utils/Terms/term_util.ML

thys/ML_Unification/ML_Utils/Theorems/ML_Theorem_Utils.thy

thys/ML_Unification/ML_Utils/Theorems/thm_util.ML

thys/ML_Unification/Normalisations/ML_Normalisations.thy

thys/ML_Unification/Normalisations/envir_normalisation.ML

thys/ML_Unification/Normalisations/term_normalisation.ML

thys/ML_Unification/README.md

thys/ML_Unification/ROOT

thys/ML_Unification/Simps_To/Simps_To.thy

thys/ML_Unification/Simps_To/simps_to.ML

thys/ML_Unification/Simps_To/simps_to_unif.ML

thys/ML_Unification/Term_Index/ML_Term_Index.thy

thys/ML_Unification/Term_Index/discrimination_tree.ML

thys/ML_Unification/Term_Index/term_index.ML

thys/ML_Unification/Term_Index/term_index_data.ML

thys/ML_Unification/Tests/First_Order_ML_Unification_Tests.thy

thys/ML_Unification/Tests/Higher_Order_ML_Unification_Tests.thy

thys/ML_Unification/Tests/Higher_Order_Pattern_ML_Unification_Tests.thy

thys/ML_Unification/Tests/ML_Unification_Tests.thy

thys/ML_Unification/Tests/ML_Unification_Tests_Base.thy

thys/ML_Unification/Tests/first_order_unification_tests.ML

thys/ML_Unification/Tests/higher_order_pattern_unification_tests.ML

thys/ML_Unification/Tests/tests_base.ML

thys/ML_Unification/Unification_Attributes/Unification_Attributes.thy

thys/ML_Unification/Unification_Attributes/unify_of.ML

thys/ML_Unification/Unification_Attributes/unify_of_base.ML

thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy

thys/ML_Unification/Unification_Hints/named_theorems_unification_hints.ML

thys/ML_Unification/Unification_Hints/term_index_unification_hints.ML

thys/ML_Unification/Unification_Hints/unification_hints.ML

thys/ML_Unification/Unification_Hints/unification_hints_base.ML

thys/ML_Unification/Unification_Parsers/ML_Unification_Parsers.thy

thys/ML_Unification/Unification_Parsers/unification_parser.ML

thys/ML_Unification/Unification_Tactics/Assumption/Unify_Assumption_Tactic.thy

thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption.ML

thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML

thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic.thy

thys/ML_Unification/Unification_Tactics/Fact/unify_fact.ML

thys/ML_Unification/Unification_Tactics/Fact/unify_fact_base.ML

thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy

thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve.ML

thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML

thys/ML_Unification/Unification_Tactics/Unification_Tactics.thy

thys/ML_Unification/Unifiers/ML_Unifiers.thy

thys/ML_Unification/Unifiers/first_order_unification.ML

thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML

thys/ML_Unification/Unifiers/higher_order_unification.ML

thys/ML_Unification/Unifiers/higher_ordern_pattern_first_decomp_unification.ML

thys/ML_Unification/Unifiers/mixed_unification.ML

thys/ML_Unification/Unifiers/simplifier_unification.ML

thys/ML_Unification/Unifiers/tactic_unification.ML

thys/ML_Unification/Unifiers/test.ML

thys/ML_Unification/Unifiers/unification_combinator.ML

thys/ML_Unification/Unifiers/unification_combine.ML

thys/ML_Unification/Unifiers/unify_copy.ML

thys/ML_Unification/document/root.bib

thys/ML_Unification/document/root.tex

thys/ML_Unification/unification_base.ML

thys/ML_Unification/unification_util.ML

thys/ROOTS