Diffusion afp-devel ce7602a023d2

feat(ML_Unification,Transport) more robust unification + new unifiers
ce7602a023d2
Actions

Tags

None

Subscribers

None

Description

feat(ML_Unification,Transport) more robust unification + new unifiers

Details

Provenance

Authored on

Parents

rAFPc86fe3a1d9eb: strengthened class parity

Branches

Unknown

Tags

Unknown

Event Timeline

kappelmann committed rAFPce7602a023d2: feat(ML_Unification,Transport) more robust unification + new unifiers.Feb 1 2024, 2:46 PM

Changes (22)

Path

Size

Examples/

E_Unification_Examples.thy

ML_Unification_HOL_Setup.thy

ML_Utils/

Tactics/

Unification_Attributes/

Unification_Attributes.thy

Unification_Hints/

ML_Unification_Hints.thy

Unification_Tactics/

Assumption/

Unify_Assumption_Tactic.thy

Fact/

Unify_Fact_Tactic.thy

Resolution/

Unify_Resolve_Tactics.thy

ML_Unifiers.thy

first_order_unification.ML

higher_order_pattern_decomp_unification.ML

higher_order_pattern_unification.ML

higher_ordern_pattern_first_decomp_unification.ML

mixed_unification.ML

simplifier_unification.ML

var_higher_order_pattern_unification.ML

unification_util.ML

Transport/

Transport/

Examples/

Prototype/

Transport_Prototype.thy

rAFPce7602a023d2

thys/ML_Unification/Examples/E_Unification_Examples.thy

Loading...

thys/ML_Unification/ML_Unification_HOL_Setup.thy

Loading...

thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML

Loading...

thys/ML_Unification/Unification_Attributes/Unification_Attributes.thy

Loading...

thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy

Loading...

thys/ML_Unification/Unification_Tactics/Assumption/Unify_Assumption_Tactic.thy

Loading...

thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic.thy

Loading...

thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy

Loading...

thys/ML_Unification/Unifiers/ML_Unifiers.thy

Loading...

thys/ML_Unification/Unifiers/first_order_unification.ML

Loading...

thys/ML_Unification/Unifiers/higher_order_pattern_decomp_unification.ML

Loading...

thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML

Loading...

thys/ML_Unification/Unifiers/higher_ordern_pattern_first_decomp_unification.ML

Loading...

thys/ML_Unification/Unifiers/mixed_unification.ML

Loading...

thys/ML_Unification/Unifiers/simplifier_unification.ML

Loading...

thys/ML_Unification/Unifiers/var_higher_order_pattern_unification.ML

Loading...

thys/ML_Unification/unification_util.ML

Loading...

thys/Transport/Transport/Examples/Prototype/Transport_Prototype.thy

Loading...

thys/Transport/Transport/Examples/Prototype/transport.ML

Loading...