Diffusion afp-devel 1335f4299090

avoid name clash
1335f4299090
Actions

Description

avoid name clash

Details

Provenance

florian.haftmann

Authored on

Parents

rAFP1a42ddd5dbbc: adapted to LuaLaTeX according to Isabelle/299f6a8faccc;

Branches

Unknown

Tags

Unknown

Event Timeline

florian.haftmann committed rAFP1335f4299090: avoid name clash.Mar 11 2021, 8:05 AM

Changes (110)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

thys/

Aggregation_Algebras/

Aggregation_Algebras.thy

Matrix_Aggregation_Algebras.thy

Algebraic_Numbers/

Compare_Complex.thy

Algebraic_VCs/

AVC_KAD/

Card_Multisets/

Coinductive/

Examples/

CCPO_Topology.thy

Hamming_Stream.thy

TLList_CCPO.thy

Concurrent_Ref_Alg/

Refinement_Lattice.thy

Containers/

CryptHOL/

Deriving/

Comparator_Generator/

Comparator.thy

Comparator_Generator.thy

Dijkstra_Shortest_Path/

Weight.thy

Formal_SSA/

Construct_SSA_notriv.thy

FormalSSA_Misc.thy

Functional_Ordered_Resolution_Prover/

Deterministic_FO_Ordered_Resolution_Prover.thy

Groebner_Bases/

Groebner_PM.thy

Groebner_Macaulay/

Hilbert_Function.thy

Hybrid_Systems_VCs/

ModalKleeneAlgebra/

HS_VC_MKA.thy

KAD/

Antidomain_Semiring.thy

Domain_Semiring.thy

Modal_Kleene_Algebra.thy

Modal_Kleene_Algebra_Applications.thy

KAT_and_DRA/

SingleSorted/

Kleene_Algebra/

Knuth_Morris_Pratt/

Lambda_Free_KBOs/

Lambda_Free_KBO_Std.thy

LatticeProperties/

Complete_Lattice_Prop.thy

Lattice_Ordered_Group.thy

Modular_Distrib_Lattice.thy

Markov_Models/

Markov_Models_Auxiliary.thy

MonoBoolTranAlgebra/

Mono_Bool_Tran_Algebra.thy

Multirelations/

C_Algebras.thy

Nested_Multisets_Ordinals/

Multiset_More.thy

Nested_Multiset.thy

Order_Lattice_Props/

Closure_Operators.thy

Order_Lattice_Props.thy

Order_Lattice_Props_Loc.thy

Ordered_Resolution_Prover/

Abstract_Substitution.thy

FO_Ordered_Resolution.thy

PAC_Checker/

More_Loops.thy

PSemigroupsConvolution/

Quantales.thy

Partial_Order_Reduction/

Extensions/

CCPO_Extensions.thy

Polynomials/

MPoly_Type_Class_OAlist.thy

MPoly_Type_Class_Ordered.thy

OAlist.thy

OAlist_Poly_Mapping.thy

Power_Products.thy

Propositional_Proof_Systems/

SC_Cut.thy

PseudoHoops/

LeftComplementedMonoid.thy

PseudoHoopFilters.thy

PseudoHoops.thy

PseudoWaisbergAlgebra.thy

SpecialPseudoHoops.thy

Quantales/

Quantale_Left_Sided.thy

Quantale_Star.thy

Quantales.thy

Quick_Sort_Cost/

Randomised_Quick_Sort.thy

Refine_Monadic/

Generic/

RefineG_Domain.thy

Refine_Misc.thy

RefinementReactive/

Temporal.thy

Regular_Algebras/

Regular_Algebra_Variants.thy

Regular_Algebras.thy

Relation_Algebra/

More_Boolean_Algebra.thy

Relation_Algebra.thy

Relation_Algebra_Functions.thy

Relation_Algebra_RTC.thy

Relation_Algebra_Tests.thy

Relational_Disjoint_Set_Forests/

Disjoint_Set_Forests.thy

Relational_Minimum_Spanning_Trees/

Boruvka.thy

Prim.thy

Relational_Paths/

More_Relation_Algebra.thy

Path_Algorithms.thy

Paths.thy

Rooted_Paths.thy

Residuated_Lattices/

Involutive_Residuated.thy

Residuated_Boolean_Algebras.thy

Residuated_Lattices.thy

Signature_Groebner/

More_MPoly.thy

Signature_Examples.thy

Signature_Groebner.thy

Simplex/

Simplex_Algebra.thy

Sqrt_Babylonian/

Sqrt_Babylonian_Auxiliary.thy

Stateful_Protocol_Composition_and_Typing/

Stone_Algebras/

Stone_Construction.thy

Stone_Kleene_Relation_Algebras/

Iterings.thy

Kleene_Algebras.thy

Kleene_Relation_Algebras.thy

Matrix_Kleene_Algebras.thy

Stone_Relation_Algebras/

Fixpoints.thy

Relation_Algebras.thy

Semirings.thy

Subset_Boolean_Algebras/

Subset_Boolean_Algebras.thy

SuperCalc/

multisets_continued.thy

Timed_Automata/

Floyd_Warshall.thy

UTP/

toolkit/

List_Extra.thy

rAFP1335f4299090

View Options

thys/Aggregation_Algebras/Aggregation_Algebras.thy

Load File

View Options

thys/Aggregation_Algebras/Matrix_Aggregation_Algebras.thy

Load File

View Options

thys/Algebraic_Numbers/Compare_Complex.thy

Load File

View Options

thys/Algebraic_VCs/AVC_KAD/VC_KAD_scratch.thy

Load File

View Options

thys/Algebraic_VCs/AVC_KAD/VC_KAD_wf.thy

Load File

View Options

thys/Algebraic_VCs/Domain_Quantale.thy

Load File

View Options

thys/Card_Multisets/Card_Multisets.thy

Load File

View Options

thys/Coinductive/Examples/CCPO_Topology.thy

Load File

View Options

thys/Coinductive/Examples/Hamming_Stream.thy

Load File

View Options

thys/Coinductive/TLList_CCPO.thy

Load File

View Options

thys/Concurrent_Ref_Alg/Refinement_Lattice.thy

Load File

View Options

thys/Containers/RBT_ext.thy

Load File

View Options

thys/Containers/Set_Impl.thy

Load File

View Options

thys/Containers/Set_Linorder.thy

Load File

View Options

thys/CryptHOL/Misc_CryptHOL.thy

Load File

View Options

thys/Deriving/Comparator_Generator/Comparator.thy

Load File

View Options

thys/Deriving/Comparator_Generator/Comparator_Generator.thy

Load File

View Options

thys/Dijkstra_Shortest_Path/Weight.thy

Load File

View Options

thys/Formal_SSA/Construct_SSA_notriv.thy

Load File

View Options

thys/Formal_SSA/FormalSSA_Misc.thy

Load File

View Options

thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy

Load File

View Options

thys/Groebner_Bases/Groebner_PM.thy

Load File

View Options

thys/Groebner_Macaulay/Hilbert_Function.thy

Load File

View Options

thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA.thy

Load File

View Options

thys/KAD/Antidomain_Semiring.thy

Load File

View Options

thys/KAD/Domain_Semiring.thy

Load File

View Options

thys/KAD/Modal_Kleene_Algebra.thy

Load File

View Options

thys/KAD/Modal_Kleene_Algebra_Applications.thy

Load File

View Options

thys/KAT_and_DRA/SingleSorted/Conway_Tests.thy

Load File

View Options

thys/KAT_and_DRA/SingleSorted/DRAT.thy

Load File

View Options

thys/KAT_and_DRA/SingleSorted/FolkTheorem.thy

Load File

View Options

thys/KAT_and_DRA/SingleSorted/KAT.thy

Load File

View Options

thys/Kleene_Algebra/Conway.thy

Load File

View Options

thys/Kleene_Algebra/DRA.thy

Load File

View Options

thys/Kleene_Algebra/Kleene_Algebra.thy

Load File

View Options

thys/Kleene_Algebra/Omega_Algebra.thy

Load File

View Options

thys/Knuth_Morris_Pratt/KMP.thy

Load File

View Options

thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy

Load File

View Options

thys/LatticeProperties/Complete_Lattice_Prop.thy

Load File

View Options

thys/LatticeProperties/Lattice_Ordered_Group.thy

Load File

View Options

thys/LatticeProperties/Modular_Distrib_Lattice.thy

Load File

View Options

thys/Markov_Models/Markov_Models_Auxiliary.thy

Load File

View Options

thys/MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy

Load File

View Options

thys/Multirelations/C_Algebras.thy

Load File

View Options

thys/Nested_Multisets_Ordinals/Multiset_More.thy

Load File

View Options

thys/Nested_Multisets_Ordinals/Nested_Multiset.thy

Load File

View Options

thys/Order_Lattice_Props/Closure_Operators.thy

Load File

View Options

thys/Order_Lattice_Props/Order_Lattice_Props.thy

Load File

View Options

thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy

Load File

View Options

thys/Ordered_Resolution_Prover/Abstract_Substitution.thy

Load File

View Options

thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy

Load File

View Options

thys/PAC_Checker/More_Loops.thy

Load File

View Options

thys/PSemigroupsConvolution/Quantales.thy

Load File

View Options

thys/Partial_Order_Reduction/Extensions/CCPO_Extensions.thy

Load File

View Options

thys/Polynomials/MPoly_Type_Class_OAlist.thy

Load File

View Options

thys/Polynomials/MPoly_Type_Class_Ordered.thy

Load File

View Options

thys/Polynomials/OAlist.thy

Load File

View Options

thys/Polynomials/OAlist_Poly_Mapping.thy

Load File

View Options

thys/Polynomials/Power_Products.thy

Load File

View Options

thys/Propositional_Proof_Systems/SC_Cut.thy

Load File

View Options

thys/PseudoHoops/LeftComplementedMonoid.thy

Load File

View Options

thys/PseudoHoops/PseudoHoopFilters.thy

Load File

View Options

thys/PseudoHoops/PseudoHoops.thy

Load File

View Options

thys/PseudoHoops/PseudoWaisbergAlgebra.thy

Load File

View Options

thys/PseudoHoops/SpecialPseudoHoops.thy

Load File

View Options

thys/Quantales/Quantale_Left_Sided.thy

Load File

View Options

thys/Quantales/Quantale_Star.thy

Load File

View Options

thys/Quantales/Quantales.thy

Load File

View Options

thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy

Load File

View Options

thys/Refine_Monadic/Generic/RefineG_Domain.thy

Load File

View Options

thys/Refine_Monadic/Refine_Misc.thy

Load File

View Options

thys/RefinementReactive/Temporal.thy

Load File

View Options

thys/Regular_Algebras/Regular_Algebra_Variants.thy

Load File

View Options

thys/Regular_Algebras/Regular_Algebras.thy

Load File

View Options

thys/Relation_Algebra/More_Boolean_Algebra.thy

Load File

View Options

thys/Relation_Algebra/Relation_Algebra.thy

Load File

View Options

thys/Relation_Algebra/Relation_Algebra_Functions.thy

Load File

View Options

thys/Relation_Algebra/Relation_Algebra_RTC.thy

Load File

View Options

thys/Relation_Algebra/Relation_Algebra_Tests.thy

Load File

View Options

thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy

Load File

View Options

thys/Relational_Minimum_Spanning_Trees/Boruvka.thy

Load File

View Options

thys/Relational_Minimum_Spanning_Trees/Prim.thy

Load File

View Options

thys/Relational_Paths/More_Relation_Algebra.thy

Load File

View Options

thys/Relational_Paths/Path_Algorithms.thy

Load File

View Options

thys/Relational_Paths/Paths.thy

Load File

View Options

thys/Relational_Paths/Rooted_Paths.thy

Load File

View Options

thys/Residuated_Lattices/Involutive_Residuated.thy

Load File

View Options

thys/Residuated_Lattices/Residuated_Boolean_Algebras.thy

Load File

View Options

thys/Residuated_Lattices/Residuated_Lattices.thy

Load File

View Options

thys/Signature_Groebner/More_MPoly.thy

Load File

View Options

thys/Signature_Groebner/Signature_Examples.thy

Load File

View Options

thys/Signature_Groebner/Signature_Groebner.thy

Load File

View Options

thys/Simplex/Simplex_Algebra.thy

Load File

View Options

thys/Sqrt_Babylonian/Sqrt_Babylonian_Auxiliary.thy

Load File

View Options

thys/Stateful_Protocol_Composition_and_Typing/Messages.thy

Load File

View Options

thys/Stone_Algebras/Filters.thy

Load File

View Options

thys/Stone_Algebras/Lattice_Basics.thy

Load File

View Options

thys/Stone_Algebras/P_Algebras.thy

Load File

View Options

thys/Stone_Algebras/Stone_Construction.thy

Load File

View Options

thys/Stone_Kleene_Relation_Algebras/Iterings.thy

Load File

View Options

thys/Stone_Kleene_Relation_Algebras/Kleene_Algebras.thy

Load File

View Options

thys/Stone_Kleene_Relation_Algebras/Kleene_Relation_Algebras.thy

Load File

View Options

thys/Stone_Kleene_Relation_Algebras/Matrix_Kleene_Algebras.thy

Load File

View Options

thys/Stone_Relation_Algebras/Fixpoints.thy

Load File

View Options

thys/Stone_Relation_Algebras/Relation_Algebras.thy

Load File

View Options

thys/Stone_Relation_Algebras/Semirings.thy

Load File

View Options

thys/Subset_Boolean_Algebras/Subset_Boolean_Algebras.thy

Load File

View Options

thys/SuperCalc/multisets_continued.thy

Load File

View Options

thys/Timed_Automata/Floyd_Warshall.thy

Load File

View Options

thys/UTP/toolkit/List_Extra.thy

Load File

avoid name clash1335f4299090Actions

Description

Details

Event Timeline

Changes (110)Show All Changes

Very Large Commit

rAFP1335f4299090

thys/Aggregation_Algebras/Aggregation_Algebras.thy

thys/Aggregation_Algebras/Matrix_Aggregation_Algebras.thy

thys/Algebraic_Numbers/Compare_Complex.thy

thys/Algebraic_VCs/AVC_KAD/VC_KAD_scratch.thy

thys/Algebraic_VCs/AVC_KAD/VC_KAD_wf.thy

thys/Algebraic_VCs/Domain_Quantale.thy

thys/Card_Multisets/Card_Multisets.thy

thys/Coinductive/Examples/CCPO_Topology.thy

thys/Coinductive/Examples/Hamming_Stream.thy

thys/Coinductive/TLList_CCPO.thy

thys/Concurrent_Ref_Alg/Refinement_Lattice.thy

thys/Containers/RBT_ext.thy

thys/Containers/Set_Impl.thy

thys/Containers/Set_Linorder.thy

thys/CryptHOL/Misc_CryptHOL.thy

thys/Deriving/Comparator_Generator/Comparator.thy

thys/Deriving/Comparator_Generator/Comparator_Generator.thy

thys/Dijkstra_Shortest_Path/Weight.thy

thys/Formal_SSA/Construct_SSA_notriv.thy

thys/Formal_SSA/FormalSSA_Misc.thy

thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy

thys/Groebner_Bases/Groebner_PM.thy

thys/Groebner_Macaulay/Hilbert_Function.thy

thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA.thy

thys/KAD/Antidomain_Semiring.thy

thys/KAD/Domain_Semiring.thy

thys/KAD/Modal_Kleene_Algebra.thy

thys/KAD/Modal_Kleene_Algebra_Applications.thy

thys/KAT_and_DRA/SingleSorted/Conway_Tests.thy

thys/KAT_and_DRA/SingleSorted/DRAT.thy

thys/KAT_and_DRA/SingleSorted/FolkTheorem.thy

thys/KAT_and_DRA/SingleSorted/KAT.thy

thys/Kleene_Algebra/Conway.thy

thys/Kleene_Algebra/DRA.thy

thys/Kleene_Algebra/Kleene_Algebra.thy

thys/Kleene_Algebra/Omega_Algebra.thy

thys/Knuth_Morris_Pratt/KMP.thy

thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy

thys/LatticeProperties/Complete_Lattice_Prop.thy

thys/LatticeProperties/Lattice_Ordered_Group.thy

thys/LatticeProperties/Modular_Distrib_Lattice.thy

thys/Markov_Models/Markov_Models_Auxiliary.thy

thys/MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy

thys/Multirelations/C_Algebras.thy

thys/Nested_Multisets_Ordinals/Multiset_More.thy

thys/Nested_Multisets_Ordinals/Nested_Multiset.thy

thys/Order_Lattice_Props/Closure_Operators.thy

thys/Order_Lattice_Props/Order_Lattice_Props.thy

thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy

thys/Ordered_Resolution_Prover/Abstract_Substitution.thy

thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy

thys/PAC_Checker/More_Loops.thy

thys/PSemigroupsConvolution/Quantales.thy

thys/Partial_Order_Reduction/Extensions/CCPO_Extensions.thy

thys/Polynomials/MPoly_Type_Class_OAlist.thy

thys/Polynomials/MPoly_Type_Class_Ordered.thy

thys/Polynomials/OAlist.thy

thys/Polynomials/OAlist_Poly_Mapping.thy

thys/Polynomials/Power_Products.thy

thys/Propositional_Proof_Systems/SC_Cut.thy

thys/PseudoHoops/LeftComplementedMonoid.thy

thys/PseudoHoops/PseudoHoopFilters.thy

thys/PseudoHoops/PseudoHoops.thy

thys/PseudoHoops/PseudoWaisbergAlgebra.thy

thys/PseudoHoops/SpecialPseudoHoops.thy

thys/Quantales/Quantale_Left_Sided.thy

thys/Quantales/Quantale_Star.thy

thys/Quantales/Quantales.thy

thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy

thys/Refine_Monadic/Generic/RefineG_Domain.thy

thys/Refine_Monadic/Refine_Misc.thy

thys/RefinementReactive/Temporal.thy

thys/Regular_Algebras/Regular_Algebra_Variants.thy

avoid name clash
1335f4299090
Actions

Changes (110)
Show All Changes