merge from afp-2023
498afcbd8371
Actions

Description

merge from afp-2023

Details

Provenance

Authored on

Parents

rAFP0e9f4ffb8a6f: Transport sitegen
rAFP04a0fb33af5c: drop SN from standard wpo-assumptions; prove irreflexivity of WPO without SN

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFP498afcbd8371: merge from afp-2023.Oct 16 2023, 1:46 AM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

04a0fb33af5c drop SN from standard wpo-assumptions; prove irreflexivity of WPO without SN
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
8047285e3ff1 added proof: the multiset extension of two orders preserves irreflexivity
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
26b4f0e402c1 added lemmas on lexicographic extension
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
9038bb20f96b added code-unfold lemma
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
8fd56a4b09e6 fix(ML_Unification) remove temporary files
Author
kappelmann
Browse Repository
No Builds
No Audits
e01b5c40b38f update hugo to 0.119.0;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
55545f12e056 moved hugo component build tool to Isabelle distribution;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
052ea9def986 update hugo component and support more platforms;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f2428fcb275d merge from afp-2023;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
736aec1d5af4 Adaption to new HOL-CSP core; some stronger compactification theorems.
Author
Burkhart Wolff <wolff@lri.fr>
Browse Repository
No Builds
No Audits
62f3ba1828fa Integrated many contributions by Benoit Ballenghuin.
Author
Burkhart Wolff <wolff@lri.fr>
Browse Repository
No Builds
No Audits
c1e65e2b7a5f merged
Author
nipkow
Browse Repository
No Builds
No Audits
1f31735d205e more lit.refs
Author
nipkow
Browse Repository
No Builds
No Audits
4f4fb5548be0 Removal of material that had already been migrated to the repository
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
b1926dc1e25f added lit.ref.
Author
nipkow
Browse Repository
No Builds
No Audits
cc8dcc3fb541 sitegen
Author
nipkow
Browse Repository
No Builds
No Audits
89c3c7db185b fix link;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9171aff43f4c sitegen
Author
nipkow
Browse Repository
No Builds
No Audits
04ff9b688095 fix url/file encoding;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
0e0c90bf2fb0 typo
Author
nipkow
Browse Repository
No Builds
No Audits
a1c1e0a73e09 typo
Author
nipkow
Browse Repository
No Builds
No Audits
42bb70bbe698 tuned metadata
Author
nipkow
Browse Repository
No Builds
No Audits
c36d06b9ec96 tuned metadata
Author
nipkow
Browse Repository
No Builds
No Audits
e6a485ed4efb tuned metadata
Author
nipkow
Browse Repository
No Builds
No Audits
14863014c6aa merged
Author
paulson
Browse Repository
No Builds
No Audits
32589d2ea562 Migration of lemmas to distribution
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
704a08d91097 merged
Author
makarius
Browse Repository
No Builds
No Audits
9c5fe84ef108 adapted to Isabelle/72631efa3821;
Author
makarius
Browse Repository
No Builds
No Audits
622d847d12a7 avoid deadly "handle _ => ...";
Author
makarius
Browse Repository
No Builds
No Audits
65c96a5ebb31 tuned: prefer try-catch/finally over low-level 'handle';
Author
makarius
Browse Repository
No Builds
No Audits
b7d5aa642fc1 tuned: prefer try-catch/finally over low-level 'handle';
Author
makarius
Browse Repository
No Builds
No Audits
02b9b8599f13 tuned: prefer try-catch/finally over low-level 'handle';
Author
makarius
Browse Repository
No Builds
No Audits
7d01367fe6b2 clarified signature, following Isabelle/fde0b195cb7d;
Author
makarius
Browse Repository
No Builds
No Audits
068d4f8c4523 adjust Euler_Polyhedron_Formula to AFP-devel
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
c984814c0dae merge from AFP 2023
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
fc96173189a3 reduced prominence of lemma names
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d57b427b0d34 merge from afp-2023
Author
kleing
Browse Repository
No Builds
No Audits
20d6a62d7fad merge from afp-2023
Author
kleing
Browse Repository
No Builds
No Audits
cd589841a170 Moved a general purpose theorem into the main repository
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
73e9fe529af2 a little fix involving the reformulated version of inclusion/exclusion
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c23d6419e9fe fixed missing parenthesis in or-ok-lemma
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
aed1fd49ef90 new bibiten and titlecase on all sections
Author
Anders Schlichtkrull <andsch@cs.aau.dk>
Browse Repository
No Builds
No Audits
bb681dd9e2f3 avoid clones of Isabelle/ML operations --- de-emphasize somewhat old/outdated…
Author
makarius
Browse Repository
No Builds
No Audits
b30dbda6bb1c replace underscore latex package with formal markup
Author
Anders Schlichtkrull <andsch@cs.aau.dk>
Browse Repository
No Builds
No Audits
bc96d1b79af3 merge
Author
Anders Schlichtkrull <andsch@cs.aau.dk>
Browse Repository
No Builds
No Audits
8f3ba551a991 fix latex generation
Author
Anders Schlichtkrull <andsch@cs.aau.dk>
Browse Repository
No Builds
No Audits
582bad32ddbf Backed out changeset 8eb0a45852dc
Author
Anders Schlichtkrull <andsch@cs.aau.dk>
Browse Repository
No Builds
No Audits
a270719ee81d tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a8a41bb5d17d avoid non-local return;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
681e992fb431 removed migration tools;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (301)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata

authors.toml

entries

Coupledsim_Contrasim.toml

IO_Language_Conformance.toml

S_Finite_Measure_Monad.toml

Standard_Borel_Spaces.toml

Transport.toml

thys

Coupledsim_Contrasim

Contrasim_Set_Game.thy

Contrasim_Word_Game.thy

Contrasimulation.thy

Coupled_Simulation.thy

Coupledsim_Fixpoint_Algo_Delay.thy

Coupledsim_Game_Delay.thy

HM_Logic_Infinitary.thy

Transition_Systems.thy

Weak_HML_Contrasimulation.thy

Weak_Relations.thy

Weak_Transition_Systems.thy

IO_Language_Conformance

Input_Output_Language_Conformance.thy

S_Finite_Measure_Monad

Kernels.thy

Lemmas_S_Finite_Measure_Monad.thy

Measure_QuasiBorel_Adjunction.thy

Standard_Borel_Spaces

Abstract_Metrizable_Topology.thy

Lemmas_StandardBorel.thy

ROOT

Set_Based_Metric_Product.thy

Set_Based_Metric_Space.thy

Space_of_Continuous_Maps.thy

Binary_Relation_Functions.thy

Binary_Relations_Lattice.thy

LBinary_Relations.thy

Order

Binary_Relations_Order.thy

Binary_Relations_Order_Base.thy

Properties

Binary_Relation_Properties.thy

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

Functions_Base.thy

LFunctions.thy

Properties

Function_Properties.thy

Functions_Bijection.thy

Functions_Injective.thy

Functions_Inverse.thy

Functions_Monotone.thy

Functions_Surjective.thy

Galois

Galois.thy

Galois_Base.thy

Galois_Connections.thy

Galois_Equivalences.thy

Galois_Property.thy

Galois_Relator.thy

Galois_Relator_Base.thy

Half_Galois_Property.thy

HOL_Alignments

HOL_Algebra_Alignment_Galois.thy

HOL_Algebra_Alignment_Orders.thy

HOL_Algebra_Alignments.thy

HOL_Alignment_Binary_Relations.thy

HOL_Alignment_Functions.thy

HOL_Alignment_Orders.thy

HOL_Syntax_Bundles.thy

HOL_Syntax_Bundles_Base.thy

HOL_Syntax_Bundles_Functions.thy

HOL_Syntax_Bundles_Groups.thy

HOL_Syntax_Bundles_Lattices.thy

HOL_Syntax_Bundles_Orders.thy

HOL_Syntax_Bundles_Relations.thy

Orders

Equivalence_Relations.thy

Functions

Closure_Operators.thy

Order_Functions.thy

Order_Functions_Base.thy

Functors

Order_Equivalences.thy

Order_Functors.thy

Order_Functors_Base.thy

Orders.thy

Partial_Equivalence_Relations.thy

Predicates_Lattice.thy

Transport_Compositions_Agree.thy

Transport_Compositions_Agree_Base.thy

Transport_Compositions_Agree_Galois_Connection.thy

Transport_Compositions_Agree_Galois_Equivalence.thy

Transport_Compositions_Agree_Galois_Property.thy

Transport_Compositions_Agree_Galois_Relator.thy

Transport_Compositions_Agree_Monotone.thy

Transport_Compositions_Agree_Order_Equivalence.thy

Generic

Transport_Compositions_Generic.thy

Transport_Compositions_Generic_Base.thy

Transport_Compositions_Generic_Galois_Connection.thy

Transport_Compositions_Generic_Galois_Equivalence.thy

Transport_Compositions_Generic_Galois_Property.thy

Transport_Compositions_Generic_Galois_Relator.thy

Transport_Compositions_Generic_Monotone.thy

Transport_Compositions_Generic_Order_Base.thy

Transport_Compositions_Generic_Order_Equivalence.thy

Transport_Compositions.thy

Examples

Prototype

Transport_Prototype.thy

Transport_Rel_If.thy

transport.ML

transport_util.ML

Transport_Dep_Fun_Rel_Examples.thy

Transport_Lists_Sets_Examples.thy

Transport_Partial_Quotient_Types.thy

Transport_Syntax.thy

Typedef

Transport_Typedef.thy

Transport_Typedef_Base.thy

Functions

Monotone_Function_Relator.thy

Reflexive_Relator.thy

Transport_Functions.thy

Transport_Functions_Base.thy

Transport_Functions_Galois_Connection.thy

Transport_Functions_Galois_Equivalence.thy

Transport_Functions_Galois_Property.thy

Transport_Functions_Galois_Relator.thy

Transport_Functions_Monotone.thy

Transport_Functions_Order_Base.thy

Transport_Functions_Order_Equivalence.thy

Transport_Functions_Relation_Simplifications.thy

Natural_Functors

Transport_Natural_Functors.thy

Transport_Natural_Functors_Base.thy

Transport_Natural_Functors_Galois.thy

Transport_Natural_Functors_Galois_Relator.thy

Transport_Natural_Functors_Order_Base.thy

Transport_Natural_Functors_Order_Equivalence.thy

Transport.thy

Transport_Base.thy

Transport_Bijections.thy

Transport_Identity.thy

Transport_Via_Partial_Galois_Connections_Equivalences_Paper.thy

bisping/

brodmann/

hirata/

jungnickel/

kappelmann/

minamide/

nestmann/

peters/

rickmann/

sachtleben/

seidler/

stueber/

weidner/

data/

standard_borel_spaces

index.html

index.xml

entries

Automated_Stateful_Protocol_Verification.html

Coupledsim_Contrasim.html

FLP.html

IO_Language_Conformance.html

KAD.html

ML_Unification.html

Multirelations.html

Relation_Algebra.html

S_Finite_Measure_Monad.html

Standard_Borel_Spaces.html

io_language_conformance

index.html

s_finite_measure_monad

index.html

standard_borel_spaces

statistics/

topics/

computer-science/

automata-and-formal-languages/

concurrency/

programming-languages/

lambda-calculi/

type-systems/

semantics-and-reasoning/

index.html

index.xml

index.html

logic/

general-logic/

index.xml

modal-logic/

index.html

index.xml

mathematics/

analysis/

games-and-economics/

measure-and-integration/

order/

probability-theory/

topology/

rAFP498afcbd8371

View Options

metadata/authors.toml

Load File

View Options

metadata/entries/Coupledsim_Contrasim.toml

Load File

View Options

metadata/entries/IO_Language_Conformance.toml

Load File

View Options

metadata/entries/S_Finite_Measure_Monad.toml

Load File

View Options

metadata/entries/Standard_Borel_Spaces.toml

Load File

View Options

metadata/entries/Transport.toml

Load File

View Options

thys/Coupledsim_Contrasim/Contrasim_Set_Game.thy

Load File

View Options

thys/Coupledsim_Contrasim/Contrasim_Word_Game.thy

Load File

View Options

thys/Coupledsim_Contrasim/Contrasimulation.thy

Load File

View Options

thys/Coupledsim_Contrasim/Coupled_Simulation.thy

Load File

View Options

thys/Coupledsim_Contrasim/Coupledsim_Fixpoint_Algo_Delay.thy

Load File

View Options

thys/Coupledsim_Contrasim/Coupledsim_Game_Delay.thy

Load File

View Options

thys/Coupledsim_Contrasim/HM_Logic_Infinitary.thy

Load File

View Options

thys/Coupledsim_Contrasim/README.md

Load File

View Options

thys/Coupledsim_Contrasim/ROOT

Load File

View Options

thys/Coupledsim_Contrasim/Simple_Game.thy

Load File

View Options

thys/Coupledsim_Contrasim/Strong_Relations.thy

Load File

View Options

thys/Coupledsim_Contrasim/Tau_Sinks.thy

Load File

View Options

thys/Coupledsim_Contrasim/Transition_Systems.thy

Load File

View Options

thys/Coupledsim_Contrasim/Weak_HML_Contrasimulation.thy

Load File

View Options

thys/Coupledsim_Contrasim/Weak_Relations.thy

Load File

View Options

thys/Coupledsim_Contrasim/Weak_Transition_Systems.thy

Load File

View Options

thys/Coupledsim_Contrasim/document/root.bib

Load File

View Options

thys/Coupledsim_Contrasim/document/root.tex

Load File

View Options

thys/Coupledsim_Contrasim/document/splncs04.bst

Load File

View Options

thys/IO_Language_Conformance/Input_Output_Language_Conformance.thy

Load File

View Options

thys/IO_Language_Conformance/ROOT

Load File

View Options

thys/IO_Language_Conformance/document/root.bib

Load File

View Options

thys/IO_Language_Conformance/document/root.tex

Load File

View Options

thys/ROOTS

Load File

View Options

thys/S_Finite_Measure_Monad/Kernels.thy

Load File

View Options

thys/S_Finite_Measure_Monad/Lemmas_S_Finite_Measure_Monad.thy

Load File

View Options

thys/S_Finite_Measure_Monad/Measure_QuasiBorel_Adjunction.thy

Load File

View Options

thys/S_Finite_Measure_Monad/Monad_QuasiBorel.thy

Load File

View Options

thys/S_Finite_Measure_Monad/Montecarlo.thy

Load File

View Options

thys/S_Finite_Measure_Monad/QBS_Morphism.thy

Load File

View Options

thys/S_Finite_Measure_Monad/QuasiBorel.thy

Load File

View Options

thys/S_Finite_Measure_Monad/Query.thy

Load File

View Options

thys/S_Finite_Measure_Monad/ROOT

Load File

View Options

thys/S_Finite_Measure_Monad/document/root.bib

Load File

View Options

thys/S_Finite_Measure_Monad/document/root.tex

Load File

View Options

thys/S_Finite_Measure_Monad/qbs.ML

Load File

View Options

thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy

Load File

View Options

thys/Standard_Borel_Spaces/Lemmas_StandardBorel.thy

Load File

View Options

thys/Standard_Borel_Spaces/ROOT

Load File

View Options

thys/Standard_Borel_Spaces/Set_Based_Metric_Product.thy

Load File

View Options

thys/Standard_Borel_Spaces/Set_Based_Metric_Space.thy

Load File

View Options

thys/Standard_Borel_Spaces/Space_of_Continuous_Maps.thy

Load File

View Options

thys/Standard_Borel_Spaces/StandardBorel.thy

Load File

View Options

thys/Standard_Borel_Spaces/document/root.bib

Load File

View Options

thys/Standard_Borel_Spaces/document/root.tex

Load File

View Options

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy

Load File

View Options

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Lattice.thy

Load File

View Options

thys/Transport/HOL_Basics/Binary_Relations/LBinary_Relations.thy

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

thys/Transport/HOL_Basics/Binary_Relations/Restricted_Equality.thy

Load File

View Options

thys/Transport/HOL_Basics/Functions/Function_Relators.thy

Load File

View Options

thys/Transport/HOL_Basics/Functions/Functions_Base.thy

Load File

View Options

thys/Transport/HOL_Basics/Functions/LFunctions.thy

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

thys/Transport/HOL_Basics/Galois/Galois.thy

Load File

View Options

thys/Transport/HOL_Basics/Galois/Galois_Base.thy

Load File

View Options

thys/Transport/HOL_Basics/Galois/Galois_Connections.thy

Load File

View Options

thys/Transport/HOL_Basics/Galois/Galois_Equivalences.thy

Load File

View Options

thys/Transport/HOL_Basics/Galois/Galois_Property.thy

Load File

View Options

thys/Transport/HOL_Basics/Galois/Galois_Relator.thy

Load File

View Options

thys/Transport/HOL_Basics/Galois/Galois_Relator_Base.thy

Load File

View Options

thys/Transport/HOL_Basics/Galois/Half_Galois_Property.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Galois.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignment_Orders.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Algebra_Alignments.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Binary_Relations.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Functions.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignment_Orders.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Alignments/HOL_Alignments.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Basics.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Basics_Base.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Mem_Of.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Base.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Functions.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Groups.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Lattices.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Orders.thy

Load File

View Options

thys/Transport/HOL_Basics/HOL_Syntax_Bundles/HOL_Syntax_Bundles_Relations.thy

Load File

View Options

thys/Transport/HOL_Basics/Orders/Equivalence_Relations.thy

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

thys/Transport/HOL_Basics/Orders/Orders.thy

Load File

View Options

thys/Transport/HOL_Basics/Orders/Partial_Equivalence_Relations.thy

Load File

View Options

thys/Transport/HOL_Basics/Orders/Partial_Orders.thy

Load File

View Options

thys/Transport/HOL_Basics/Orders/Preorders.thy

Load File

View Options

thys/Transport/HOL_Basics/Predicates/Predicates.thy

Load File

View Options

thys/Transport/HOL_Basics/Predicates/Predicates_Lattice.thy

Load File

View Options

thys/Transport/HOL_Basics/Predicates/Predicates_Order.thy

Load File

View Options

thys/Transport/README.md

Load File

View Options

thys/Transport/ROOT

Load File

View Options

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree.thy

Load File

View Options

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Base.thy

Load File

View Options

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Connection.thy

Load File

View Options

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Equivalence.thy

Load File

View Options

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Galois_Property.thy

Load File

View Options

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

Load File

View Options

thys/Transport/Transport/Compositions/Agree/Transport_Compositions_Agree_Monotone.thy

Load File

View Options

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

Load File

View Options

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic.thy

Load File

View Options

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

Load File

View Options

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Connection.thy

Load File

View Options

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Equivalence.thy

Load File

View Options

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Galois_Property.thy

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

thys/Transport/Transport/Compositions/Generic/Transport_Compositions_Generic_Order_Equivalence.thy

Load File

View Options

thys/Transport/Transport/Compositions/Transport_Compositions.thy

Load File

View Options

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

Load File

View Options

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

Load File

View Options

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

Load File

View Options

thys/Transport/Transport/Examples/Prototype/transport_util.ML

Load File

View Options

thys/Transport/Transport/Examples/Transport_Dep_Fun_Rel_Examples.thy

Load File

View Options

thys/Transport/Transport/Examples/Transport_Lists_Sets_Examples.thy

Load File

View Options

thys/Transport/Transport/Examples/Transport_Partial_Quotient_Types.thy

Load File

View Options

thys/Transport/Transport/Examples/Transport_Syntax.thy

Load File

View Options

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

Load File

View Options

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

Load File

View Options

thys/Transport/Transport/Functions/Monotone_Function_Relator.thy

Load File

View Options

thys/Transport/Transport/Functions/Reflexive_Relator.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Base.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Galois_Connection.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Galois_Equivalence.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Galois_Property.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Galois_Relator.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Monotone.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Order_Base.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Order_Equivalence.thy

Load File

View Options

thys/Transport/Transport/Functions/Transport_Functions_Relation_Simplifications.thy

Load File

View Options

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors.thy

Load File

View Options

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Base.thy

Load File

View Options

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Galois.thy

Load File

View Options

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Galois_Relator.thy

Load File

View Options

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Base.thy

Load File

View Options

thys/Transport/Transport/Natural_Functors/Transport_Natural_Functors_Order_Equivalence.thy

Load File

View Options

thys/Transport/Transport/Transport.thy

Load File

View Options

thys/Transport/Transport/Transport_Base.thy

Load File

View Options

thys/Transport/Transport/Transport_Bijections.thy

Load File

View Options

thys/Transport/Transport/Transport_Identity.thy

Load File

View Options

thys/Transport/Transport/Transport_Via_Partial_Galois_Connections_Equivalences_Paper.thy

Load File

View Options

thys/Transport/document/root.bib

Load File

View Options

thys/Transport/document/root.tex

Load File

View Options

web/authors/bisping/index.html

Load File

View Options

web/authors/bisping/index.xml

Load File

View Options

web/authors/brodmann/index.html

Load File

View Options

web/authors/hirata/index.html

Load File

View Options

web/authors/hirata/index.xml

Load File

View Options

web/authors/index.html

Load File

View Options

web/authors/index.json

Load File

View Options

web/authors/jungnickel/index.html

Load File

View Options

web/authors/kappelmann/index.html

Load File

View Options

web/authors/kappelmann/index.xml

Load File

View Options

web/authors/minamide/index.html

Load File

View Options

web/authors/minamide/index.xml

Load File

View Options

web/authors/montanari/index.html

Load File

View Options

web/authors/montanari/index.xml

Load File

View Options

web/authors/nestmann/index.html

Load File

View Options

web/authors/peters/index.html

Load File

View Options

web/authors/rickmann/index.html

Load File

View Options

web/authors/sachtleben/index.html

Load File

View Options

web/authors/sachtleben/index.xml

Load File

View Options

web/authors/seidler/index.html

Load File

View Options

web/authors/stueber/index.html

Load File

View Options

web/authors/weidner/index.html

Load File

View Options

web/data/keywords.json

Load File

View Options

web/dependencies/index.html

Load File

View Options

web/dependencies/index.json

Load File

View Options

web/dependencies/ml_unification/index.html

Load File

View Options

web/dependencies/ml_unification/index.xml

Load File

View Options

web/dependencies/standard_borel_spaces/index.html

Load File

View Options

web/dependencies/standard_borel_spaces/index.xml

Load File

View Options

web/entries/Automated_Stateful_Protocol_Verification.html

Load File

View Options

web/entries/Coupledsim_Contrasim.html

Load File

View Options

web/entries/FLP.html

Load File

View Options

web/entries/IO_Language_Conformance.html

Load File

View Options

web/entries/KAD.html

Load File

View Options

web/entries/ML_Unification.html

Load File

View Options

web/entries/Multirelations.html

Load File

View Options

web/entries/Relation_Algebra.html

Load File

View Options

web/entries/S_Finite_Measure_Monad.html

Load File

View Options

web/entries/Standard_Borel_Spaces.html

Load File

View Options

web/entries/Transport.html

Load File

View Options

web/entries/index.html

Load File

View Options

web/entries/index.xml

Load File

View Options

web/index.html

Load File

View Options

web/index.json

Load File

View Options

web/index.xml

Load File

View Options

web/sessions/coupledsim_contrasim/index.html

Load File

View Options

web/sessions/index.xml

Load File

View Options

web/sessions/io_language_conformance/index.html

Load File

View Options

web/sessions/s_finite_measure_monad/index.html

Load File

View Options

web/sessions/standard_borel_spaces/index.html

Load File

View Options

web/sessions/transport/index.html

Load File

View Options

web/sitemap.xml

Load File

View Options

web/statistics/index.html

Load File

View Options

web/topics/computer-science/automata-and-formal-languages/index.html

Load File

View Options

web/topics/computer-science/automata-and-formal-languages/index.xml

Load File

View Options

web/topics/computer-science/concurrency/index.html

Load File

View Options

web/topics/computer-science/concurrency/index.xml

Load File

View Options

web/topics/computer-science/index.xml

Load File

View Options

web/topics/computer-science/programming-languages/index.xml

Load File

View Options

web/topics/computer-science/programming-languages/lambda-calculi/index.html

Load File

View Options

web/topics/computer-science/programming-languages/lambda-calculi/index.xml

Load File

View Options

web/topics/computer-science/programming-languages/type-systems/index.html

Load File

View Options

web/topics/computer-science/programming-languages/type-systems/index.xml

Load File

View Options

web/topics/computer-science/semantics-and-reasoning/index.html

Load File

View Options

web/topics/computer-science/semantics-and-reasoning/index.xml

Load File

View Options

web/topics/index.html

Load File

View Options

web/topics/logic/general-logic/index.xml

Load File

View Options

web/topics/logic/general-logic/modal-logic/index.html

Load File

View Options

web/topics/logic/general-logic/modal-logic/index.xml

Load File

View Options

web/topics/logic/index.xml

Load File

View Options

web/topics/mathematics/analysis/index.html

Load File

View Options

web/topics/mathematics/analysis/index.xml

Load File

View Options

web/topics/mathematics/games-and-economics/index.html

Load File

View Options

web/topics/mathematics/games-and-economics/index.xml

Load File

View Options

web/topics/mathematics/index.xml

Load File

View Options

web/topics/mathematics/measure-and-integration/index.html

Load File

View Options

web/topics/mathematics/measure-and-integration/index.xml

Load File

View Options

web/topics/mathematics/order/index.html

Load File

View Options

web/topics/mathematics/order/index.xml

Load File

View Options

web/topics/mathematics/probability-theory/index.html

Load File

View Options

web/topics/mathematics/probability-theory/index.xml

Load File

View Options

web/topics/mathematics/topology/index.html

Load File

View Options

web/topics/mathematics/topology/index.xml

Load File

merge from afp-2023498afcbd8371Actions

Description

Details

Event Timeline

Merged Changes

Changes (301)Show All Changes

Very Large Commit

rAFP498afcbd8371

metadata/authors.toml

metadata/entries/Coupledsim_Contrasim.toml

metadata/entries/IO_Language_Conformance.toml

metadata/entries/S_Finite_Measure_Monad.toml

metadata/entries/Standard_Borel_Spaces.toml

metadata/entries/Transport.toml

thys/Coupledsim_Contrasim/Contrasim_Set_Game.thy

thys/Coupledsim_Contrasim/Contrasim_Word_Game.thy

thys/Coupledsim_Contrasim/Contrasimulation.thy

thys/Coupledsim_Contrasim/Coupled_Simulation.thy

thys/Coupledsim_Contrasim/Coupledsim_Fixpoint_Algo_Delay.thy

thys/Coupledsim_Contrasim/Coupledsim_Game_Delay.thy

thys/Coupledsim_Contrasim/HM_Logic_Infinitary.thy

thys/Coupledsim_Contrasim/README.md

thys/Coupledsim_Contrasim/ROOT

thys/Coupledsim_Contrasim/Simple_Game.thy

thys/Coupledsim_Contrasim/Strong_Relations.thy

thys/Coupledsim_Contrasim/Tau_Sinks.thy

thys/Coupledsim_Contrasim/Transition_Systems.thy

thys/Coupledsim_Contrasim/Weak_HML_Contrasimulation.thy

thys/Coupledsim_Contrasim/Weak_Relations.thy

thys/Coupledsim_Contrasim/Weak_Transition_Systems.thy

thys/Coupledsim_Contrasim/document/root.bib

thys/Coupledsim_Contrasim/document/root.tex

thys/Coupledsim_Contrasim/document/splncs04.bst

thys/IO_Language_Conformance/Input_Output_Language_Conformance.thy

thys/IO_Language_Conformance/ROOT

thys/IO_Language_Conformance/document/root.bib

thys/IO_Language_Conformance/document/root.tex

thys/ROOTS

thys/S_Finite_Measure_Monad/Kernels.thy

thys/S_Finite_Measure_Monad/Lemmas_S_Finite_Measure_Monad.thy

thys/S_Finite_Measure_Monad/Measure_QuasiBorel_Adjunction.thy

thys/S_Finite_Measure_Monad/Monad_QuasiBorel.thy

thys/S_Finite_Measure_Monad/Montecarlo.thy

thys/S_Finite_Measure_Monad/QBS_Morphism.thy

thys/S_Finite_Measure_Monad/QuasiBorel.thy

thys/S_Finite_Measure_Monad/Query.thy

thys/S_Finite_Measure_Monad/ROOT

thys/S_Finite_Measure_Monad/document/root.bib

thys/S_Finite_Measure_Monad/document/root.tex

thys/S_Finite_Measure_Monad/qbs.ML

thys/Standard_Borel_Spaces/Abstract_Metrizable_Topology.thy

thys/Standard_Borel_Spaces/Lemmas_StandardBorel.thy

thys/Standard_Borel_Spaces/ROOT

thys/Standard_Borel_Spaces/Set_Based_Metric_Product.thy

thys/Standard_Borel_Spaces/Set_Based_Metric_Space.thy

thys/Standard_Borel_Spaces/Space_of_Continuous_Maps.thy

thys/Standard_Borel_Spaces/StandardBorel.thy

thys/Standard_Borel_Spaces/document/root.bib

thys/Standard_Borel_Spaces/document/root.tex

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relation_Functions.thy

thys/Transport/HOL_Basics/Binary_Relations/Binary_Relations_Lattice.thy

thys/Transport/HOL_Basics/Binary_Relations/LBinary_Relations.thy

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

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

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

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

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

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

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

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

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

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

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

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

thys/Transport/HOL_Basics/Binary_Relations/Restricted_Equality.thy

thys/Transport/HOL_Basics/Functions/Function_Relators.thy

thys/Transport/HOL_Basics/Functions/Functions_Base.thy

thys/Transport/HOL_Basics/Functions/LFunctions.thy

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

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

merge from afp-2023
498afcbd8371
Actions

Changes (301)
Show All Changes