HomeIsabelle/Phabricator
Diffusion afp-devel e1dd89a2f035

feat(ML_Unification) add simplification+unification unifier; fix context merge…
e1dd89a2f035
Actions

Description

feat(ML_Unification) add simplification+unification unifier; fix context merge bug for uhints; cleaner code

Details

Provenance
kappelmannAuthored on
Parents
rAFPce7602a023d2: feat(ML_Unification,Transport) more robust unification + new unifiers
Branches
Unknown
Tags
Unknown

Changes (50)

PathSize
Examples/
Logger/
ML_Utils/
Tactics/
Theorems/
Normalisations/
Simps_To/
Term_Index/
Tests/

rAFPe1dd89a2f035

View Options

thys/ML_Unification/Examples/E_Unification_Examples.thy

Loading...
View Options

thys/ML_Unification/Examples/Unification_Hints_Reification_Examples.thy

Loading...
View Options

thys/ML_Unification/Logger/ML_Logger_Examples.thy

Loading...
View Options

thys/ML_Unification/Logger/logger.ML

Loading...
View Options

thys/ML_Unification/ML_Unification_HOL_Setup.thy

Loading...
View Options

thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML

Loading...
View Options

thys/ML_Unification/ML_Utils/Theorems/thm_util.ML

Loading...
View Options

thys/ML_Unification/Normalisations/envir_normalisation.ML

Loading...
View Options

thys/ML_Unification/Simps_To/Simps_To.thy

Loading...
View Options

thys/ML_Unification/Simps_To/simps_to.ML

Loading...
View Options

thys/ML_Unification/Simps_To/simps_to_unif.ML

Loading...
View Options

thys/ML_Unification/Term_Index/discrimination_tree.ML

Loading...
View Options

thys/ML_Unification/Term_Index/term_index.ML

Loading...
View Options

thys/ML_Unification/Term_Index/term_index_data.ML

Loading...
View Options

thys/ML_Unification/Tests/First_Order_ML_Unification_Tests.thy

Loading...
View Options

thys/ML_Unification/Tests/Higher_Order_Pattern_ML_Unification_Tests.thy

Loading...
View Options

thys/ML_Unification/Tests/ML_Unification_Tests_Base.thy

Loading...
View Options

thys/ML_Unification/Unification_Attributes/Unification_Attributes.thy

Loading...
View Options

thys/ML_Unification/Unification_Attributes/Unification_Attributes_Base.thy

Loading...
View Options

thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy

Loading...
View Options

thys/ML_Unification/Unification_Hints/ML_Unification_Hints_Base.thy

Loading...
View Options

thys/ML_Unification/Unification_Hints/term_index_unification_hints.ML

Loading...
View Options

thys/ML_Unification/Unification_Hints/unification_hints_base.ML

Loading...
View Options

thys/ML_Unification/Unification_Tactics/Assumption/Unify_Assumption_Tactic.thy

Loading...
View Options

thys/ML_Unification/Unification_Tactics/Assumption/Unify_Assumption_Tactic_Base.thy

Loading...
View Options

thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic.thy

Loading...
View Options

thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic_Base.thy

Loading...
View Options

thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy

Loading...
View Options

thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics_Base.thy

Loading...
View Options

thys/ML_Unification/Unifiers/ML_Unifiers.thy

Loading...
View Options

thys/ML_Unification/Unifiers/ML_Unifiers_Base.thy

Loading...
View Options

thys/ML_Unification/Unifiers/higher_order_pattern_decomp_unification.ML

Loading...
View Options

thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML

Loading...
View Options

thys/ML_Unification/Unifiers/higher_order_unification.ML

Loading...
View Options

thys/ML_Unification/Unifiers/mixed_unification.ML

Loading...
View Options

thys/ML_Unification/Unifiers/simplifier_unification.ML

Loading...
View Options

thys/ML_Unification/Unifiers/tactic_unification.ML

Loading...
View Options

thys/ML_Unification/Unifiers/type_unification.ML

Loading...
View Options

thys/ML_Unification/Unifiers/unification_combinator.ML

Loading...
View Options

thys/ML_Unification/Unifiers/var_higher_order_pattern_unification.ML

Loading...
View Options

thys/ML_Unification/unification_base.ML

Loading...