feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems…
fe57a84f565f
Actions

Description

feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems up to alpha (and not alpha-eta) equivalence, fix wrong bounded variables substitution

feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems…fe57a84f565fActions

Description

Details

Event Timeline

Changes (33)

rAFPfe57a84f565f

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/ML_Unification_Base.thy

thys/ML_Unification/ML_Unification_HOL_Setup.thy

thys/ML_Unification/ML_Utils/Conversions/ML_Conversion_Utils.thy

thys/ML_Unification/ML_Utils/Conversions/conversion_util.ML

thys/ML_Unification/ML_Utils/General/general_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/tactic_util.ML

thys/ML_Unification/ML_Utils/Terms/term_util.ML

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/ROOT

thys/ML_Unification/Simps_To/simps_to_unif.ML

thys/ML_Unification/Tests/First_Order_ML_Unification_Tests.thy

thys/ML_Unification/Tests/Higher_Order_Pattern_ML_Unification_Tests.thy

thys/ML_Unification/Tests/tests_base.ML

thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy

thys/ML_Unification/Unification_Hints/unification_hints_base.ML

thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_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/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/simplifier_unification.ML

thys/ML_Unification/unification_base.ML

thys/ML_Unification/unification_util.ML

feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems…
fe57a84f565f
Actions