Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

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

Summary

  1. merge
  2. merge
  3. merge
  4. feat(Transport) tune naming, updates from ML_Unification
  5. feat(ML_Unification) index hints on lhs and rhs term
  6. feat(Transport) more uniform concepts for and notation for monotonicity
  7. feat(Transport) infix for eval, improve some text
  8. fix(Transport) replace deleted elim theorem
  9. feat(Transport) remove two superfluous bin_rel lemmas
Changeset 14390:1977483c46a7 by kevin kappelmann _kevin.kappelmann@tum.de_:
merge
Changeset 14389:c30179244966 by kevin kappelmann _kevin.kappelmann@tum.de_:
merge
Changeset 14388:16398c3495e3 by kevin kappelmann _kevin.kappelmann@tum.de_:
merge
Changeset 14387:7d29a998b4a9 by kevin kappelmann _kevin.kappelmann@tum.de_:
feat(Transport) tune naming, updates from ML_Unification
The file was modified thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Dependent_Binary_Relations.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Clean_Function.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Base.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Evaluation.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Extend.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Lambda.thy
The file was modified thys/Transport/HOL_Basics/Functions/Function_Relators.thy
The file was modified thys/Transport/Transport/Examples/Prototype/Transport_Prototype.thy
Changeset 14386:094ba6117789 by kevin kappelmann _kevin.kappelmann@tum.de_:
feat(ML_Unification) index hints on lhs and rhs term
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/Unification_Hints/ML_Unification_Hints.thy
The file was modified thys/ML_Unification/Unification_Hints/term_index_unification_hints.ML
Changeset 14385:1578a3b29551 by kevin kappelmann _kevin.kappelmann@tum.de_:
feat(Transport) more uniform concepts for and notation for monotonicity
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Agree.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Extend.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Dependent_Binary_Relations.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Clean_Function.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Base.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Composition.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Extend.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Lambda.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/Functions/Properties/Functions_Bijection.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/Galois/Galois_Connections.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/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/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_Connection.thy
The file was modified thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Equivalence.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_Rel_If.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/Transport_Bijections.thy
Changeset 14384:cd87ec293c0b by kevin kappelmann _kevin.kappelmann@tum.de_:
feat(Transport) infix for eval, improve some text
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Dependent_Binary_Relations.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Clean_Function.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Base.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Evaluation.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Injective.thy
Changeset 14383:191af98a6c94 by kevin kappelmann _kevin.kappelmann@tum.de_:
fix(Transport) replace deleted elim theorem
The file was modified thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Galois.thy
Changeset 14382:b9671736f160 by kevin kappelmann _kevin.kappelmann@tum.de_:
feat(Transport) remove two superfluous bin_rel lemmas
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy
The file was modified thys/Transport/HOL_Basics/Binary_Relations/Dependent_Binary_Relations.thy