Diffusion afp-devel 0ef06b1fd5fe

feat(ML_Unification) fix exceptions and improve experience wrt. flex-flex…
0ef06b1fd5fe
Actions

Tags

None

Subscribers

None

Description

feat(ML_Unification) fix exceptions and improve experience wrt. flex-flex instantiations

Details

Provenance

Authored on

Parents

rAFP0b447dd0606c: fix(ML_Unification) use cartouches to fix document build error

Branches

Unknown

Tags

Unknown

Event Timeline

kappelmann committed rAFP0ef06b1fd5fe: feat(ML_Unification) fix exceptions and improve experience wrt. flex-flex….Jan 19 2024, 6:12 PM

Changes (13)

Path

Size

thys/

ML_Unification/

Logger/

ML_Unification_Base.thy

ML_Utils/

Tactics/

ML_Tactic_Utils.thy

Theorems/

ML_Theorem_Utils.thy

Unification_Tactics/

Assumption/

unify_assumption_base.ML

Fact/

Unify_Fact_Tactic.thy

Resolution/

unify_resolve_base.ML

Unifiers/

higher_order_unification.ML

unification_base.ML

unification_util.ML

Transport/

Transport/

Examples/

Prototype/

rAFP0ef06b1fd5fe

thys/ML_Unification/Logger/logger.ML

Loading...

thys/ML_Unification/ML_Unification_Base.thy

Loading...

thys/ML_Unification/ML_Utils/Tactics/ML_Tactic_Utils.thy

Loading...

thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML

Loading...

thys/ML_Unification/ML_Utils/Theorems/ML_Theorem_Utils.thy

Loading...

thys/ML_Unification/ML_Utils/Theorems/thm_util.ML

Loading...

thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML

Loading...

thys/ML_Unification/Unification_Tactics/Fact/Unify_Fact_Tactic.thy

Loading...

thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML

Loading...

thys/ML_Unification/Unifiers/higher_order_unification.ML

Loading...

thys/ML_Unification/unification_base.ML

Loading...

thys/ML_Unification/unification_util.ML

Loading...

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

Loading...