Diffusion afp-devel eb74b5bcfc8c

feat(Transport) better relativised concept definitions and lemmas
eb74b5bcfc8c
Actions

Tags

None

Subscribers

None

Description

feat(Transport) better relativised concept definitions and lemmas

Details

Provenance

Authored on

Parents

rAFP9412dd83073e: feat(ML_Unification) add recursive unification hints fallback option

Branches

Unknown

Tags

Unknown

Event Timeline

kappelmann committed rAFPeb74b5bcfc8c: feat(Transport) better relativised concept definitions and lemmas.Jan 4 2024, 5:57 PM

Changes (59)

Path

Size

thys/

Transport/

HOL_Basics/

Binary_Relations/

Binary_Relation_Functions.thy

Binary_Relations_Lattice.thy

Order/

Binary_Relations_Order_Base.thy

Properties/

Binary_Relations_Antisymmetric.thy

Binary_Relations_Injective.thy

Binary_Relations_Irreflexive.thy

Binary_Relations_Left_Total.thy

Binary_Relations_Reflexive.thy

Binary_Relations_Right_Unique.thy

Binary_Relations_Surjective.thy

Binary_Relations_Symmetric.thy

Binary_Relations_Transitive.thy

Restricted_Equality.thy

Functions/

Function_Relators.thy

Properties/

Functions_Bijection.thy

Functions_Injective.thy

Functions_Inverse.thy

Functions_Monotone.thy

Functions_Surjective.thy

Galois/

Galois_Relator.thy

Galois_Relator_Base.thy

Half_Galois_Property.thy

HOL_Alignments/

HOL_Algebra_Alignment_Galois.thy

HOL_Alignment_Binary_Relations.thy

HOL_Alignment_Functions.thy

Orders/

Equivalence_Relations.thy

Functions/

Closure_Operators.thy

Order_Functions_Base.thy

Functors/

Order_Functors_Base.thy

Partial_Equivalence_Relations.thy

Partial_Orders.thy

Predicates/

Transport/

Compositions/

Agree/

Transport_Compositions_Agree_Galois_Relator.thy

Transport_Compositions_Agree_Order_Equivalence.thy

Generic/

Transport_Compositions_Generic_Base.thy

Transport_Compositions_Generic_Galois_Relator.thy

Transport_Compositions_Generic_Monotone.thy

Transport_Compositions_Generic_Order_Base.thy

Examples/

Prototype/

Transport_Prototype.thy

Transport_Rel_If.thy

Transport_Partial_Quotient_Types.thy

Typedef/

Transport_Typedef.thy

Transport_Typedef_Base.thy

Functions/

Monotone_Function_Relator.thy

Reflexive_Relator.thy

Transport_Functions.thy

Transport_Functions_Galois_Connection.thy

Transport_Functions_Galois_Equivalence.thy

Transport_Functions_Galois_Relator.thy

Transport_Functions_Order_Base.thy

Transport_Functions_Order_Equivalence.thy

Natural_Functors/

Transport_Natural_Functors_Base.thy

Transport_Natural_Functors_Galois_Relator.thy

Transport_Natural_Functors_Order_Base.thy

Transport_Bijections.thy

document/

rAFPeb74b5bcfc8c

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Lattice.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Order/Binary_Relations_Order_Base.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Antisymmetric.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Injective.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Irreflexive.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Left_Total.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Reflexive.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Right_Unique.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Surjective.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Symmetric.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Properties/Binary_Relations_Transitive.thy

Loading...

thys/Transport/HOL_Basics/Binary_Relations/Restricted_Equality.thy

Loading...

thys/Transport/HOL_Basics/Functions/Function_Relators.thy

Loading...

thys/Transport/HOL_Basics/Functions/Properties/Functions_Bijection.thy

Loading...

thys/Transport/HOL_Basics/Functions/Properties/Functions_Injective.thy

Loading...

thys/Transport/HOL_Basics/Functions/Properties/Functions_Inverse.thy

Loading...

thys/Transport/HOL_Basics/Functions/Properties/Functions_Monotone.thy

Loading...

thys/Transport/HOL_Basics/Functions/Properties/Functions_Surjective.thy

Loading...

thys/Transport/HOL_Basics/Galois/Galois_Relator.thy

Loading...

thys/Transport/HOL_Basics/Galois/Galois_Relator_Base.thy

Loading...

thys/Transport/HOL_Basics/Galois/Half_Galois_Property.thy

Loading...

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Galois.thy

Loading...

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Binary_Relations.thy

Loading...

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Functions.thy

Loading...

thys/Transport/HOL_Basics/Orders/Equivalence_Relations.thy

Loading...

thys/Transport/HOL_Basics/Orders/Functions/Closure_Operators.thy

Loading...

thys/Transport/HOL_Basics/Orders/Functions/Order_Functions_Base.thy

Loading...

thys/Transport/HOL_Basics/Orders/Functors/Order_Functors_Base.thy

Loading...

thys/Transport/HOL_Basics/Orders/Partial_Equivalence_Relations.thy

Loading...

thys/Transport/HOL_Basics/Orders/Partial_Orders.thy

Loading...

thys/Transport/HOL_Basics/Orders/Preorders.thy

Loading...

thys/Transport/HOL_Basics/Predicates/Predicates.thy

Loading...

thys/Transport/ROOT

Loading...

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Relator.thy

Loading...

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Order_Equivalence.thy

Loading...

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Base.thy

Loading...

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Relator.thy

Loading...

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Monotone.thy

Loading...

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Order_Base.thy

Loading...

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

Loading...

thys/Transport/Transport/Examples/Prototype/Transport_Rel_If.thy

Loading...

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

Loading...

thys/Transport/Transport/Examples/Transport_Partial_Quotient_Types.thy

Loading...

thys/Transport/Transport/Examples/Typedef/Transport_Typedef.thy

Loading...

thys/Transport/Transport/Examples/Typedef/Transport_Typedef_Base.thy

Loading...

thys/Transport/Transport/Functions/Monotone_Function_Relator.thy

Loading...

thys/Transport/Transport/Functions/Reflexive_Relator.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Galois_Connection.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Galois_Equivalence.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Galois_Relator.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Order_Base.thy

Loading...

thys/Transport/Transport/Functions/Transport_Functions_Order_Equivalence.thy

Loading...

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Base.thy

Loading...

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Galois_Relator.thy

Loading...

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Base.thy

Loading...

thys/Transport/Transport/Transport_Bijections.thy

Loading...

thys/Transport/document/root.bib

Loading...