Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. feat(Transport) add simpler function type introduction rule for extend
  3. feat(Transport) functions as binary relations, improved mono notation, make non-dependent relators definitions, generalise some concepts
  4. feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems up to alpha (and not alpha-eta) equivalence, fix wrong bounded variables substitution
Changeset 14316:3133b6848037 by kevin kappelmann _kevin.kappelmann@tum.de_:
merged
Changeset 14315:2a6196e5b347 by kevin kappelmann _kevin.kappelmann@tum.de_:
feat(Transport) add simpler function type introduction rule for extend
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Extend.thy
Changeset 14314:237996782d80 by kevin kappelmann _kevin.kappelmann@tum.de_:
feat(Transport) functions as binary relations, improved mono notation, make non-dependent relators definitions, generalise some concepts
The file was addedthys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Agree.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Extend.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Dependent_Binary_Relations.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Clean_Function.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Base.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Composition.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Evaluation.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Extend.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Lambda.thy
The file was addedthys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Connected.thy
The file was addedthys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Predicates.thy
The file was addedthys/Transport/HOL_Basics/Orders/Linear_Orders.thy
The file was addedthys/Transport/HOL_Basics/Predicates/Bounded_Definite_Description.thy
The file was addedthys/Transport/HOL_Basics/Predicates/Bounded_Quantifiers.thy
The file was addedthys/Transport/HOL_Basics/Predicates/Predicate_Functions.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/LBinary_Relations.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relation_Properties.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Antisymmetric.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Injective.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Left_Total.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Reflexive.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Right_Unique.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Surjective.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Symmetric.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Transitive.thy
The file was modified thys/Transport/HOL_Basics/Functions/Function_Relators.thy
The file was modified thys/Transport/HOL_Basics/Functions/Functions_Base.thy
The file was modified thys/Transport/HOL_Basics/Functions/Functions_Restrict.thy
The file was modified thys/Transport/HOL_Basics/Functions/LFunctions.thy
The file was modified thys/Transport/HOL_Basics/Functions/Properties/Functions_Bijection.thy
The file was modified thys/Transport/HOL_Basics/Functions/Properties/Functions_Injective.thy
The file was modified thys/Transport/HOL_Basics/Functions/Properties/Functions_Inverse.thy
The file was modified thys/Transport/HOL_Basics/Functions/Properties/Functions_Monotone.thy
The file was modified thys/Transport/HOL_Basics/Functions/Properties/Functions_Surjective.thy
The file was modified thys/Transport/HOL_Basics/Galois/Galois.thy
The file was modified thys/Transport/HOL_Basics/Galois/Galois_Property.thy
The file was modified thys/Transport/HOL_Basics/Galois/Galois_Relator.thy
The file was modified thys/Transport/HOL_Basics/Galois/Half_Galois_Property.thy
The file was modified thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Galois.thy
The file was modified thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Orders.thy
The file was modified thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Binary_Relations.thy
The file was modified thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Functions.thy
The file was modified thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Orders.thy
The file was modified thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignments.thy
The file was modified thys/Transport/HOL_Basics/HOL_Basics.thy
The file was modified thys/Transport/HOL_Basics/HOL_Basics_Base.thy
The file was modified thys/Transport/HOL_Basics/HOL_Mem_Of.thy
The file was modified thys/Transport/HOL_Basics/Orders/Functions/Closure_Operators.thy
The file was modified thys/Transport/HOL_Basics/Orders/Functions/Order_Functions_Base.thy
The file was modified thys/Transport/HOL_Basics/Orders/Functors/Order_Equivalences.thy
The file was modified thys/Transport/HOL_Basics/Orders/Functors/Order_Functors_Base.thy
The file was modified thys/Transport/HOL_Basics/Orders/Orders.thy
The file was modified thys/Transport/HOL_Basics/Predicates/Predicates.thy
The file was modified thys/Transport/HOL_Basics/Predicates/Predicates_Order.thy
The file was modified thys/Transport/ROOT
The file was modified thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Connection.thy
The file was modified thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Equivalence.thy
The file was modified thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Property.thy
The file was modified thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Relator.thy
The file was modified thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Monotone.thy
The file was modified thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Order_Equivalence.thy
The file was modified thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Base.thy
The file was modified thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Property.thy
The file was modified thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Relator.thy
The file was modified thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Monotone.thy
The file was modified thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Order_Base.thy
The file was modified thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Order_Equivalence.thy
The file was modified thys/Transport/Transport/Examples/Prototype/Transport_Prototype.thy
The file was modified thys/Transport/Transport/Examples/Prototype/Transport_Rel_If.thy
The file was modified thys/Transport/Transport/Examples/Prototype/transport.ML
The file was modified thys/Transport/Transport/Examples/Transport_Dep_Fun_Rel_Examples.thy
The file was modified thys/Transport/Transport/Examples/Transport_Lists_Sets_Examples.thy
The file was modified thys/Transport/Transport/Examples/Transport_Partial_Quotient_Types.thy
The file was modified thys/Transport/Transport/Examples/Typedef/Transport_Typedef.thy
The file was modified thys/Transport/Transport/Functions/Monotone_Function_Relator.thy
The file was modified thys/Transport/Transport/Functions/Reflexive_Relator.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Base.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Galois_Connection.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Galois_Equivalence.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Galois_Property.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Galois_Relator.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Monotone.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Order_Base.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Order_Equivalence.thy
The file was modified thys/Transport/Transport/Functions/Transport_Functions_Relation_Simplifications.thy
The file was modified thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Base.thy
The file was modified thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Equivalence.thy
Changeset 14313:fe57a84f565f by kevin kappelmann _kevin.kappelmann@tum.de_:
feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems up to alpha (and not alpha-eta) equivalence, fix wrong bounded variables substitution
The file was modified thys/ML_Unification/Binders/binders.ML
The file was modified thys/ML_Unification/Examples/E_Unification_Examples.thy
The file was modified thys/ML_Unification/Examples/Unification_Hints_Reification_Examples.thy
The file was modified thys/ML_Unification/ML_Unification_Base.thy
The file was modified thys/ML_Unification/ML_Unification_HOL_Setup.thy
The file was modified thys/ML_Unification/ML_Utils/Conversions/ML_Conversion_Utils.thy
The file was modified thys/ML_Unification/ML_Utils/Conversions/conversion_util.ML
The file was modified thys/ML_Unification/ML_Utils/General/general_util.ML
The file was modified thys/ML_Unification/ML_Utils/Priorities/ML_Priorities.thy
The file was modified thys/ML_Unification/ML_Utils/Priorities/priority.ML
The file was modified thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML
The file was modified thys/ML_Unification/ML_Utils/Terms/term_util.ML
The file was modified thys/ML_Unification/ML_Utils/Theorems/thm_util.ML
The file was modified thys/ML_Unification/Normalisations/ML_Normalisations.thy
The file was modified thys/ML_Unification/Normalisations/envir_normalisation.ML
The file was modified thys/ML_Unification/ROOT
The file was modified thys/ML_Unification/Simps_To/simps_to_unif.ML
The file was modified thys/ML_Unification/Tests/First_Order_ML_Unification_Tests.thy
The file was modified thys/ML_Unification/Tests/Higher_Order_Pattern_ML_Unification_Tests.thy
The file was modified thys/ML_Unification/Tests/tests_base.ML
The file was modified thys/ML_Unification/Unification_Hints/ML_Unification_Hints.thy
The file was modified thys/ML_Unification/Unification_Hints/unification_hints_base.ML
The file was modified thys/ML_Unification/Unification_Tactics/Assumption/unify_assumption_base.ML
The file was modified thys/ML_Unification/Unification_Tactics/Resolution/Unify_Resolve_Tactics.thy
The file was modified thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve.ML
The file was modified thys/ML_Unification/Unification_Tactics/Resolution/unify_resolve_base.ML
The file was modified thys/ML_Unification/Unifiers/ML_Unifiers.thy
The file was modified thys/ML_Unification/Unifiers/first_order_unification.ML
The file was modified thys/ML_Unification/Unifiers/higher_order_pattern_unification.ML
The file was modified thys/ML_Unification/Unifiers/higher_order_unification.ML
The file was modified thys/ML_Unification/Unifiers/simplifier_unification.ML
The file was modified thys/ML_Unification/unification_base.ML
The file was modified thys/ML_Unification/unification_util.ML