HomeIsabelle/Phabricator
Diffusion afp-devel 975b2b1d8a19

renamed hide_lams opaque_lifting
975b2b1d8a19
Actions

Description

renamed hide_lams opaque_lifting

Details

Provenance
desharnaAuthored on
Parents
rAFP9c417896a51d: Added missing Public_Announcement_Logic to ROOTS file
Branches
Unknown
Tags
Unknown

Changes (394)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.
PathSize
thys/
AI_Planning_Languages_Semantics/
AODV/
variants/
a_norreqid/
b_fwdrreps/
c_gtobcast/
d_fwdrreqs/
e_all_abcd/
AWN/
Adaptive_State_Counting/
ASC/
ATC/
FSM/
Affine_Arithmetic/
Aggregation_Algebras/
Algebraic_Numbers/
Amicable_Numbers/
Approximation_Algorithms/
Automated_Stateful_Protocol_Verification/
Automatic_Refinement/
Lib/
BTree/
Banach_Steinhaus/
BenOr_Kozen_Reif/
Berlekamp_Zassenhaus/
Bicategory/
Binding_Syntax_Theory/
BirdKMP/
Budan_Fourier/
Buildings/
CAVA_Automata/
CISC-Kernel/
trace/
Rushby-with-Control/
CakeML_Codegen/
Backend/
Call_Arity/
Chandy_Lamport/
Coinductive/
Examples/
Collections/
GenCF/
Gen/
Complex_Geometry/
ComponentDependencies/
ConcurrentGC/
ConcurrentIMP/
Consensus_Refined/
Observing/
Constructive_Cryptography_CM/
Constructions/
Containers/
Examples/
Core_DOM/
common/
monads/
standard/
Core_SC_DOM/
common/
monads/
safely_composable/
Count_Complex_Roots/
CryptHOL/
DOM_Components/
Decreasing-Diagrams/
Dependent_SIFUM_Refinement/
Examples/
Dependent_SIFUM_Type_Systems/
Derangements/
Differential_Game_Logic/
DiscretePricing/
Echelon_Form/
Epistemic_Logic/
Ergodic_Theory/
Extended_Finite_State_Machine_Inference/
Extended_Finite_State_Machines/
FLP/
Featherweight_OCL/
collection_types/
Formal_SSA/
Formula_Derivatives/
FunWithFunctions/
Functional_Ordered_Resolution_Prover/
Gabow_SCC/
Gauss_Jordan/
Generic_Join/
Graph_Theory/
Green/
Groebner_Bases/
Gromov_Hyperbolicity/
Grothendieck_Schemes/
HOL-CSP/
Hoare_Time/
Hybrid_Logic/
Hybrid_Multi_Lane_Spatial_Logic/
regular/
Hybrid_Systems_VCs/
KleeneAlgebraTests/
ModalKleeneAlgebra/
PredicateTransformers/
HyperCTL/
IMAP-CRDT/
IMP2/
basic/
IP_Addresses/
Impossible_Geometry/
Inductive_Inference/
Interval_Arithmetic_Word32/
Iptables_Semantics/
Semantics_Ternary/
Irrational_Series_Erdos_Straus/
Irrationality_J_Hancl/
IsaGeoCoq/
Isabelle_Marries_Dirac/
Jacobson_Basic_Algebra/
KAD/
KAT_and_DRA/
SingleSorted/
TwoSorted/
Kleene_Algebra/
Knot_Theory/
Koenigsberg_Friendship/
Kruskal/
Kuratowski_Closure_Complement/
LLL_Basis_Reduction/
LLL_Factorization/
LOFT/
LTL_Master_Theorem/
LTL_to_DRA/
Logical_Characterization/
LTL_to_DRA/
Launchbury/
LinearQuantifierElim/
Thys/
Linear_Programming/
Linear_Recurrences/
List-Index/
LocalLexing/
Localization_Ring/
Lp/
Lucas_Theorem/
MFMC_Countable/
MFOTL_Monitor/
MSO_Regex_Equivalence/
Matrices_for_ODEs/
Matrix_Tensor/
Metalogic_ProofChecker/
Modal_Logics_for_NTS/
Modular_arithmetic_LLL_and_HNF_algorithms/
Monad_Memo_DP/
example/
MonoBoolTranAlgebra/
Multi_Party_Computation/
Multirelations/
Nested_Multisets_Ordinals/
Network_Security_Policy_Verification/
Neumann_Morgenstern_Utility/
Octonions/
Optics/
Order_Lattice_Props/
Ordered_Resolution_Prover/
Ordinal_Partitions/
Ordinary_Differential_Equations/
IVP/
Library/
Numerics/
PAC_Checker/
PLM/
Padic_Ints/
Partial_Order_Reduction/
Extensions/
Perfect-Number-Thm/
Physical_Quantities/
Planarity_Certificates/
Verification/
Poincare_Bendixson/
Poincare_Disc/
Polynomial_Factorization/
Polynomials/
Prim_Dijkstra_Simple/
Progress_Tracking/
Projective_Geometry/
Projective_Measurements/
Propositional_Proof_Systems/
QHLProver/
QR_Decomposition/
Quantales/
Rank_Nullity_Theorem/
Real_Impl/
Refine_Imperative_HOL/
IICF/
Impl/
Heaps/
RefinementReactive/
Regex_Equivalence/
Regular-Sets/
Regular_Algebras/
Relational_Disjoint_Set_Forests/
Relational_Minimum_Spanning_Trees/
Relational_Paths/
Residuated_Lattices/
Ribbon_Proofs/
SC_DOM_Components/
SIFUM_Type_Systems/
Safe_Distance/
Shadow_DOM/
monads/
Shadow_SC_DOM/
Sigma_Commit_Crypto/
Smith_Normal_Form/
Smooth_Manifolds/
Sort_Encodings/
Source_Coding_Theorem/
Stable_Matching/
Stateful_Protocol_Composition_and_Typing/
Stone_Algebras/
Stone_Kleene_Relation_Algebras/
Stone_Relation_Algebras/
Sturm_Tarski/
Subset_Boolean_Algebras/
SuperCalc/
Syntax_Independent_Logic/
Timed_Automata/
Topological_Semantics/
Transformer_Semantics/
Transition_Systems_and_Automata/
Basic/
Tree_Decomposition/
Twelvefold_Way/
UPF_Firewall/
FWNormalisation/
UTP/
toolkit/
utp/
VectorSpace/
Vickrey_Clarke_Groves/
WHATandWHERE_Security/
WOOT_Strong_Eventual_Consistency/
WebAssembly/
Winding_Number_Eval/
Word_Lib/
ZFC_in_HOL/

rAFP975b2b1d8a19

View Options

thys/AI_Planning_Languages_Semantics/PDDL_STRIPS_Semantics.thy

View Options

thys/AI_Planning_Languages_Semantics/SASP_Checker.thy

View Options

thys/AODV/Fresher.thy

View Options

thys/AODV/variants/a_norreqid/A_Fresher.thy

View Options

thys/AODV/variants/b_fwdrreps/B_Fresher.thy

View Options

thys/AODV/variants/c_gtobcast/C_Fresher.thy

View Options

thys/AODV/variants/d_fwdrreqs/D_Fresher.thy

View Options

thys/AODV/variants/e_all_abcd/E_Fresher.thy

View Options

thys/AWN/Pnet.thy

View Options

thys/Adaptive_State_Counting/ASC/ASC_Sufficiency.thy

View Options

thys/Adaptive_State_Counting/ASC/ASC_Suite.thy

View Options

thys/Adaptive_State_Counting/ATC/ATC.thy

View Options

thys/Adaptive_State_Counting/FSM/FSM.thy

View Options

thys/Affine_Arithmetic/Affine_Form.thy

View Options

thys/Affine_Arithmetic/Floatarith_Expression.thy

View Options

thys/Affine_Arithmetic/Intersection.thy

View Options

thys/Aggregation_Algebras/Matrix_Aggregation_Algebras.thy

View Options

thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy

View Options

thys/Amicable_Numbers/Amicable_Numbers.thy

View Options

thys/Approximation_Algorithms/Approx_BP_Hoare.thy

View Options

thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy

View Options

thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy

View Options

thys/Automated_Stateful_Protocol_Verification/Term_Implication.thy

View Options

thys/Automatic_Refinement/Lib/Misc.thy

View Options

thys/BTree/BTree_ImpSplit.thy

View Options

thys/BTree/BTree_Set.thy

View Options

thys/Banach_Steinhaus/Banach_Steinhaus.thy

View Options

thys/Banach_Steinhaus/Banach_Steinhaus_Missing.thy

View Options

thys/BenOr_Kozen_Reif/BKR_Decision.thy

View Options

thys/BenOr_Kozen_Reif/Matrix_Equation_Construction.thy

View Options

thys/BenOr_Kozen_Reif/Renegar_Decision.thy

View Options

thys/BenOr_Kozen_Reif/Renegar_Proofs.thy

View Options

thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy

View Options

thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy

View Options

thys/Berlekamp_Zassenhaus/Distinct_Degree_Factorization.thy

View Options

thys/Bicategory/SpanBicategory.thy

View Options

thys/Binding_Syntax_Theory/Iteration.thy

View Options

thys/Binding_Syntax_Theory/Semantic_Domains.thy

View Options

thys/Binding_Syntax_Theory/Transition_QuasiTerms_Terms.thy

View Options

thys/BirdKMP/HOLCF_ROOT.thy

View Options

thys/BirdKMP/KMP.thy

View Options

thys/Budan_Fourier/BF_Misc.thy

View Options

thys/Buildings/Algebra.thy

View Options

thys/CAVA_Automata/Simulation.thy

View Options

thys/CISC-Kernel/trace/Rushby-with-Control/SK.thy

View Options

thys/CakeML_Codegen/Backend/CakeML_Correctness.thy

View Options

thys/Call_Arity/ArityAnalysisAbinds.thy

View Options

thys/Call_Arity/CoCallImplSafe.thy

View Options

thys/Chandy_Lamport/Snapshot.thy

View Options

thys/Chandy_Lamport/Swap.thy

View Options

thys/Chandy_Lamport/Util.thy

View Options

thys/Coinductive/Examples/LMirror.thy

View Options

thys/Collections/GenCF/Gen/Gen_Map.thy

View Options

thys/Complex_Geometry/Linear_Systems.thy

View Options

thys/Complex_Geometry/More_Complex.thy

View Options

thys/Complex_Geometry/More_Transcendental.thy

View Options

thys/ComponentDependencies/DataDependenciesCaseStudy.thy

View Options

thys/ConcurrentGC/Global_Invariants_Lemmas.thy

View Options

thys/ConcurrentGC/Local_Invariants_Lemmas.thy

View Options

thys/ConcurrentGC/Noninterference.thy

View Options

thys/ConcurrentGC/StrongTricolour.thy

View Options

thys/ConcurrentIMP/Infinite_Sequences.thy

View Options

thys/ConcurrentIMP/LTL.thy

View Options

thys/Consensus_Refined/Observing/BenOr_Proofs.thy

View Options

thys/Constructive_Cryptography_CM/Constructions/One_Time_Pad.thy

View Options

thys/Containers/Examples/Containers_TwoSat_Ex.thy

View Options

thys/Core_DOM/common/Core_DOM_Functions.thy

View Options

thys/Core_DOM/common/monads/CharacterDataMonad.thy

View Options

thys/Core_DOM/common/monads/DocumentMonad.thy

View Options

thys/Core_DOM/common/monads/ElementMonad.thy

View Options

thys/Core_DOM/standard/Core_DOM_Heap_WF.thy

View Options

thys/Core_SC_DOM/common/Core_DOM_Functions.thy

View Options

thys/Core_SC_DOM/common/monads/CharacterDataMonad.thy

View Options

thys/Core_SC_DOM/common/monads/DocumentMonad.thy

View Options

thys/Core_SC_DOM/common/monads/ElementMonad.thy

View Options

thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy

View Options

thys/Count_Complex_Roots/Count_Complex_Roots.thy

View Options

thys/Count_Complex_Roots/More_Polynomials.thy

View Options

thys/CryptHOL/GPV_Expectation.thy

View Options

thys/DOM_Components/Core_DOM_Components.thy

View Options

thys/Decreasing-Diagrams/Decreasing_Diagrams.thy

View Options

thys/Dependent_SIFUM_Refinement/Examples/Eg1Eg2RefinementSimple.thy

View Options

thys/Dependent_SIFUM_Refinement/Examples/EgHighBranchRevC.thy

View Options

thys/Dependent_SIFUM_Type_Systems/Compositionality.thy

View Options

thys/Dependent_SIFUM_Type_Systems/LocallySoundModeUse.thy

View Options

thys/Dependent_SIFUM_Type_Systems/TypeSystem.thy

View Options

thys/Derangements/Derangements.thy

View Options

thys/Differential_Game_Logic/Coincidence.thy

View Options

thys/Differential_Game_Logic/USubst.thy

View Options

thys/DiscretePricing/CRR_Model.thy

View Options

thys/DiscretePricing/Disc_Cond_Expect.thy

View Options

thys/DiscretePricing/Fair_Price.thy

View Options

thys/DiscretePricing/Infinite_Coin_Toss_Space.thy

View Options

thys/Echelon_Form/Echelon_Form.thy

View Options

thys/Echelon_Form/Echelon_Form_IArrays.thy

View Options

thys/Epistemic_Logic/Epistemic_Logic.thy

View Options

thys/Ergodic_Theory/Invariants.thy

View Options

thys/Ergodic_Theory/Normalizing_Sequences.thy

View Options

thys/Ergodic_Theory/Transfer_Operator.thy

View Options

thys/Extended_Finite_State_Machine_Inference/Subsumption.thy

View Options

thys/Extended_Finite_State_Machines/Trilean.thy

View Options

thys/FLP/Execution.thy

View Options

thys/FLP/FLPTheorem.thy

View Options

thys/Featherweight_OCL/UML_PropertyProfiles.thy

View Options

thys/Featherweight_OCL/UML_State.thy

View Options

thys/Featherweight_OCL/collection_types/UML_Bag.thy

View Options

thys/Featherweight_OCL/collection_types/UML_Set.thy

View Options

thys/Formal_SSA/FormalSSA_Misc.thy

View Options

thys/Formula_Derivatives/WS1S_Formula.thy

View Options

thys/FunWithFunctions/FunWithFunctions.thy

View Options

thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy

View Options

thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy

View Options

thys/Gabow_SCC/Gabow_Skeleton.thy

View Options

thys/Gauss_Jordan/Determinants2.thy

View Options

thys/Gauss_Jordan/Elementary_Operations.thy

View Options

thys/Gauss_Jordan/Inverse.thy

View Options

thys/Gauss_Jordan/Linear_Maps.thy

View Options

thys/Gauss_Jordan/System_Of_Equations.thy

View Options

thys/Generic_Join/Generic_Join_Correctness.thy

View Options

thys/Graph_Theory/Digraph_Component.thy

View Options

thys/Green/CircExample.thy

View Options

thys/Green/DiamExample.thy

View Options

thys/Green/Paths.thy

View Options

thys/Groebner_Bases/Algorithm_Schema.thy

View Options

thys/Gromov_Hyperbolicity/Bonk_Schramm_Extension.thy

View Options

thys/Gromov_Hyperbolicity/Busemann_Function.thy

View Options

thys/Gromov_Hyperbolicity/Eexp_Eln.thy

View Options

thys/Gromov_Hyperbolicity/Gromov_Boundary.thy

View Options

thys/Gromov_Hyperbolicity/Gromov_Hyperbolicity.thy

View Options

thys/Gromov_Hyperbolicity/Isometries_Classification.thy

View Options

thys/Gromov_Hyperbolicity/Library_Complements.thy

View Options

thys/Gromov_Hyperbolicity/Morse_Gromov_Theorem.thy

View Options

thys/Grothendieck_Schemes/Comm_Ring.thy

View Options

thys/HOL-CSP/CSP.thy

View Options

thys/HOL-CSP/Mndet.thy

View Options

thys/HOL-CSP/Sync.thy

View Options

thys/Hoare_Time/Big_StepT_Partial.thy

View Options

thys/Hoare_Time/QuantK_Hoare.thy

View Options

thys/Hoare_Time/Quant_Hoare.thy

View Options

thys/Hybrid_Logic/Hybrid_Logic.thy

View Options

thys/Hybrid_Multi_Lane_Spatial_Logic/HMLSL.thy

View Options

thys/Hybrid_Multi_Lane_Spatial_Logic/Length.thy

View Options

thys/Hybrid_Multi_Lane_Spatial_Logic/NatInt.thy

View Options

thys/Hybrid_Multi_Lane_Spatial_Logic/RealInt.thy

View Options

thys/Hybrid_Multi_Lane_Spatial_Logic/Restriction.thy

View Options

thys/Hybrid_Multi_Lane_Spatial_Logic/Sensors.thy

View Options

thys/Hybrid_Multi_Lane_Spatial_Logic/Views.thy

View Options

thys/Hybrid_Multi_Lane_Spatial_Logic/regular/Regular_Sensors.thy

View Options

thys/Hybrid_Systems_VCs/HS_VC_Examples.thy

View Options

thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_ndfun.thy

View Options

thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_rel.thy

View Options

thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_ndfun.thy

View Options

thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_rel.thy

View Options

thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT_Examples.thy

View Options

thys/HyperCTL/Finite_Noninterference.thy

View Options

thys/IMAP-CRDT/IMAP-proof-independent.thy

View Options

thys/IMP2/basic/Semantics.thy

View Options

thys/IP_Addresses/Prefix_Match.thy

View Options

thys/Impossible_Geometry/Impossible_Geometry.thy

View Options

thys/Inductive_Inference/Universal.thy

View Options

thys/Interval_Arithmetic_Word32/Finite_String.thy

View Options

thys/Interval_Arithmetic_Word32/Interval_Word32.thy

View Options

thys/Iptables_Semantics/Semantics_Embeddings.thy

View Options

thys/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy

View Options

thys/Irrational_Series_Erdos_Straus/Irrational_Series_Erdos_Straus.thy

View Options

thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy

View Options

thys/IsaGeoCoq/Tarski_Neutral.thy

View Options

thys/Isabelle_Marries_Dirac/Deutsch_Jozsa.thy

View Options

thys/Isabelle_Marries_Dirac/Measurement.thy

View Options

thys/Isabelle_Marries_Dirac/Quantum_Teleportation.thy

View Options

thys/Jacobson_Basic_Algebra/Group_Theory.thy

View Options

thys/KAD/Antidomain_Semiring.thy

View Options

thys/KAT_and_DRA/SingleSorted/Test_Dioid.thy

View Options

thys/KAT_and_DRA/TwoSorted/DRAT2.thy

View Options

thys/Kleene_Algebra/Dioid_Models.thy

View Options

thys/Kleene_Algebra/Kleene_Algebra_Models.thy

View Options

thys/Knot_Theory/Example.thy

View Options

thys/Knot_Theory/Kauffman_Matrix.thy

View Options

thys/Koenigsberg_Friendship/KoenigsbergBridge.thy

View Options

thys/Koenigsberg_Friendship/MoreGraph.thy

View Options

thys/Kruskal/Kruskal_Misc.thy

View Options

thys/Kuratowski_Closure_Complement/KuratowskiClosureComplementTheorem.thy

View Options

thys/LLL_Basis_Reduction/Gram_Schmidt_Int.thy

View Options

thys/LLL_Factorization/LLL_Factorization.thy

View Options

thys/LLL_Factorization/Missing_Dvd_Int_Poly.thy

View Options

thys/LOFT/LinuxRouter_OpenFlow_Translation.thy

View Options

thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy

View Options

thys/LTL_Master_Theorem/LTL_to_DRA/Transition_Functions.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy

View Options

thys/LTL_to_DRA/Logical_Characterization.thy

View Options

thys/LTL_to_DRA/Mojmir.thy

View Options

thys/LTL_to_DRA/Semi_Mojmir.thy

View Options

thys/Launchbury/Env.thy

View Options

thys/Launchbury/Nominal-Utils.thy

View Options

thys/LinearQuantifierElim/Thys/FRE.thy

View Options

thys/Linear_Programming/Matrix_LinPoly.thy

View Options

thys/Linear_Recurrences/Rational_FPS_Solver.thy

View Options

thys/List-Index/List_Index.thy

View Options

thys/LocalLexing/Derivations.thy

View Options

thys/LocalLexing/Ladder.thy

View Options

thys/LocalLexing/PathLemmas.thy

View Options

thys/LocalLexing/TheoremD14.thy

View Options

thys/LocalLexing/TheoremD5.thy

View Options

thys/LocalLexing/Validity.thy

View Options

thys/Localization_Ring/Localization.thy

View Options

thys/Lp/Functional_Spaces.thy

View Options

thys/Lucas_Theorem/Lucas_Theorem.thy

View Options

thys/MFMC_Countable/MFMC_Unbounded.thy

View Options

thys/MFMC_Countable/Matrix_For_Marginals.thy

View Options

thys/MFOTL_Monitor/Table.thy

View Options

thys/MSO_Regex_Equivalence/Pi_Regular_Exp_Dual.thy

View Options

thys/Matrices_for_ODEs/MTX_Flows.thy

View Options

thys/Matrices_for_ODEs/MTX_Preliminaries.thy

View Options

thys/Matrix_Tensor/Matrix_Tensor.thy

View Options

thys/Metalogic_ProofChecker/Logic.thy

View Options

thys/Metalogic_ProofChecker/Name.thy

View Options

thys/Metalogic_ProofChecker/SortsExe.thy

View Options

thys/Metalogic_ProofChecker/Term_Subst.thy

View Options

thys/Modal_Logics_for_NTS/FL_Formula.thy

View Options

thys/Modal_Logics_for_NTS/FL_Validity.thy

View Options

thys/Modal_Logics_for_NTS/Formula.thy

View Options

thys/Modal_Logics_for_NTS/L_Transform.thy

View Options

thys/Modal_Logics_for_NTS/Residual.thy

View Options

thys/Modal_Logics_for_NTS/S_Transform.thy

View Options

thys/Modal_Logics_for_NTS/Transition_System.thy

View Options

thys/Modal_Logics_for_NTS/Weak_Transition_System.thy

View Options

thys/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy

View Options

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Storjohann.thy

View Options

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Uniqueness_Hermite_JNF.thy

View Options

thys/Monad_Memo_DP/example/Bellman_Ford.thy

View Options

thys/MonoBoolTranAlgebra/Statements.thy

View Options

thys/Multi_Party_Computation/Malicious_OT.thy

View Options

thys/Multirelations/Multirelations.thy

View Options

thys/Nested_Multisets_Ordinals/Duplicate_Free_Multiset.thy

View Options

thys/Network_Security_Policy_Verification/TopoS_Helper.thy

View Options

thys/Network_Security_Policy_Verification/TopoS_Stateful_Policy.thy

View Options

thys/Neumann_Morgenstern_Utility/Neumann_Morgenstern_Utility_Theorem.thy

View Options

thys/Octonions/Cross_Product_7.thy

View Options

thys/Optics/Lens_Order.thy

View Options

thys/Optics/Scenes.thy

View Options

thys/Order_Lattice_Props/Fixpoint_Fusion.thy

View Options

thys/Order_Lattice_Props/Galois_Connections.thy

View Options

thys/Order_Lattice_Props/Order_Lattice_Props.thy

View Options

thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy

View Options

thys/Order_Lattice_Props/Order_Lattice_Props_Wenzel.thy

View Options

thys/Order_Lattice_Props/Representations.thy

View Options

thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy

View Options

thys/Ordinal_Partitions/Erdos_Milner.thy

View Options

thys/Ordinal_Partitions/Library_Additions.thy

View Options

thys/Ordinal_Partitions/Omega_Omega.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Cones.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Flow.thy

View Options

thys/Ordinary_Differential_Equations/Library/Linear_ODE.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy

View Options

thys/PAC_Checker/PAC_More_Poly.thy

View Options

thys/PAC_Checker/PAC_Specification.thy

View Options

thys/PLM/TAO_5_MetaSolver.thy

View Options

thys/Padic_Ints/Cring_Poly.thy

View Options

thys/Padic_Ints/Function_Ring.thy

View Options

thys/Padic_Ints/Hensels_Lemma.thy

View Options

thys/Padic_Ints/Padic_Integers.thy

View Options

thys/Padic_Ints/Zp_Compact.thy

View Options

thys/Partial_Order_Reduction/Extensions/Set_Extensions.thy

View Options

thys/Perfect-Number-Thm/Sigma.thy

View Options

thys/Physical_Quantities/Power_int.thy

View Options

thys/Planarity_Certificates/Verification/Check_Non_Planarity_Verification.thy

View Options

thys/Poincare_Bendixson/Analysis_Misc.thy

View Options

thys/Poincare_Bendixson/Poincare_Bendixson.thy

View Options

thys/Poincare_Disc/Poincare_Between.thy

View Options

thys/Poincare_Disc/Poincare_Tarski.thy

View Options

thys/Polynomial_Factorization/Missing_List.thy

View Options

thys/Polynomials/MPoly_PM.thy

View Options

thys/Polynomials/MPoly_Type_Class.thy

View Options

thys/Polynomials/MPoly_Type_Class_Ordered.thy

View Options

thys/Polynomials/More_MPoly_Type.thy

View Options

thys/Prim_Dijkstra_Simple/Directed_Graph_Specs.thy

View Options

thys/Progress_Tracking/Exchange.thy

View Options

thys/Progress_Tracking/Exchange_Abadi.thy

View Options

thys/Projective_Geometry/Desargues_2D.thy

View Options

thys/Projective_Measurements/CHSH_Inequality.thy

View Options

thys/Propositional_Proof_Systems/CNF_Formulas.thy

View Options

thys/Propositional_Proof_Systems/HC_Compl_Consistency.thy

View Options

thys/Propositional_Proof_Systems/Resolution_Compl_Consistency.thy

View Options

thys/QHLProver/Matrix_Limit.thy

View Options

thys/QR_Decomposition/Least_Squares_Approximation.thy

View Options

thys/QR_Decomposition/Miscellaneous_QR.thy

View Options

thys/QR_Decomposition/QR_Decomposition.thy

View Options

thys/QR_Decomposition/QR_Efficient.thy

View Options

thys/Quantales/Dioid_Models_New.thy

View Options

thys/Quantales/Quantale_Left_Sided.thy

View Options

thys/Quantales/Quantale_Modules.thy

View Options

thys/Quantales/Quantales.thy

View Options

thys/Quantales/Quantic_Nuclei_Conuclei.thy

View Options

thys/Rank_Nullity_Theorem/Mod_Type.thy

View Options

thys/Real_Impl/Real_Unique_Impl.thy

View Options

thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heapmap.thy

View Options

thys/Refine_Imperative_HOL/IICF/Impl/IICF_Array_Matrix.thy

View Options

thys/RefinementReactive/Refinement.thy

View Options

thys/Regex_Equivalence/Deriv_Autos.thy

View Options

thys/Regular-Sets/pEquivalence_Checking.thy

View Options

thys/Regular_Algebras/Regular_Algebra_Models.thy

View Options

thys/Regular_Algebras/Regular_Algebras.thy

View Options

thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy

View Options

thys/Relational_Minimum_Spanning_Trees/Kruskal.thy

View Options

thys/Relational_Minimum_Spanning_Trees/Prim.thy

View Options

thys/Relational_Paths/Path_Algorithms.thy

View Options

thys/Residuated_Lattices/Residuated_Boolean_Algebras.thy

View Options

thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy

View Options

thys/SC_DOM_Components/Core_DOM_DOM_Components.thy

View Options

thys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy

View Options

thys/SC_DOM_Components/Shadow_DOM_SC_DOM_Components.thy

View Options

thys/SIFUM_Type_Systems/Compositionality.thy

View Options

thys/SIFUM_Type_Systems/LocallySoundModeUse.thy

View Options

thys/SIFUM_Type_Systems/Preliminaries.thy

View Options

thys/SIFUM_Type_Systems/TypeSystem.thy

View Options

thys/Safe_Distance/Safe_Distance_Reaction.thy

View Options

thys/Shadow_DOM/Shadow_DOM.thy

View Options

thys/Shadow_DOM/monads/ShadowRootMonad.thy

View Options

thys/Shadow_SC_DOM/Shadow_DOM.thy

View Options

thys/Sigma_Commit_Crypto/Chaum_Pedersen_Sigma_Commit.thy

View Options

thys/Sigma_Commit_Crypto/Okamoto_Sigma_Commit.thy

View Options

thys/Sigma_Commit_Crypto/Rivest.thy

View Options

thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy

View Options

thys/Smith_Normal_Form/Cauchy_Binet.thy

View Options

thys/Smith_Normal_Form/Diagonal_To_Smith.thy

View Options

thys/Smith_Normal_Form/Elementary_Divisor_Rings.thy

View Options

thys/Smith_Normal_Form/Finite_Field_Mod_Type_Connection.thy

View Options

thys/Smith_Normal_Form/Rings2_Extended.thy

View Options

thys/Smith_Normal_Form/SNF_Algorithm.thy

View Options

thys/Smith_Normal_Form/SNF_Algorithm_Euclidean_Domain.thy

View Options

thys/Smooth_Manifolds/Projective_Space.thy

View Options

thys/Sort_Encodings/G.thy

View Options

thys/Sort_Encodings/M.thy

View Options

thys/Sort_Encodings/T.thy

View Options

thys/Source_Coding_Theorem/Source_Coding_Theorem.thy

View Options

thys/Stable_Matching/Sotomayor.thy

View Options

thys/Stable_Matching/Strategic.thy

View Options

thys/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy

View Options

thys/Stateful_Protocol_Composition_and_Typing/More_Unification.thy

View Options

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy

View Options

thys/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy

View Options

thys/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy

View Options

thys/Stone_Algebras/Stone_Construction.thy

View Options

thys/Stone_Kleene_Relation_Algebras/Kleene_Relation_Algebras.thy

View Options

thys/Stone_Kleene_Relation_Algebras/Matrix_Kleene_Algebras.thy

View Options

thys/Stone_Relation_Algebras/Fixpoints.thy

View Options

thys/Stone_Relation_Algebras/Linear_Order_Matrices.thy

View Options

thys/Stone_Relation_Algebras/Matrix_Relation_Algebras.thy

View Options

thys/Stone_Relation_Algebras/Relation_Algebras.thy

View Options

thys/Stone_Relation_Algebras/Relation_Subalgebras.thy

View Options

thys/Sturm_Tarski/Sturm_Tarski.thy

View Options

thys/Subset_Boolean_Algebras/Subset_Boolean_Algebras.thy

View Options

thys/SuperCalc/superposition.thy

View Options

thys/Syntax_Independent_Logic/Deduction_Q.thy

View Options

thys/Syntax_Independent_Logic/Syntax.thy

View Options

thys/Syntax_Independent_Logic/Syntax_Arith.thy

View Options

thys/Timed_Automata/DBM_Operations.thy

View Options

thys/Topological_Semantics/ex_LFUs.thy

View Options

thys/Topological_Semantics/topo_operators_basic.thy

View Options

thys/Transformer_Semantics/Isotone_Transformers.thy

View Options

thys/Transformer_Semantics/Kleisli_Transformers.thy

View Options

thys/Transformer_Semantics/Powerset_Monad.thy

View Options

thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy

View Options

thys/Tree_Decomposition/Graph.thy

View Options

thys/Twelvefold_Way/Equiv_Relations_on_Functions.thy

View Options

thys/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy

View Options

thys/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy

View Options

thys/UTP/toolkit/List_Extra.thy

View Options

thys/UTP/toolkit/Map_Extra.thy

View Options

thys/UTP/utp/utp_concurrency.thy

View Options

thys/UTP/utp/utp_rel_laws.thy

View Options

thys/UTP/utp/utp_rel_opsem.thy

View Options

thys/UTP/utp/utp_subst.thy

View Options

thys/UTP/utp/utp_var.thy

View Options

thys/VectorSpace/LinearCombinations.thy

View Options

thys/Vickrey_Clarke_Groves/Argmax.thy

View Options

thys/Vickrey_Clarke_Groves/MiscTools.thy

View Options

thys/Vickrey_Clarke_Groves/SetUtils.thy

View Options

thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy

View Options

thys/Vickrey_Clarke_Groves/Universes.thy

View Options

thys/WHATandWHERE_Security/Parallel_Composition.thy

View Options

thys/WOOT_Strong_Eventual_Consistency/IntegrateInsertCommute.thy

View Options

thys/WOOT_Strong_Eventual_Consistency/Psi.thy

View Options

thys/WOOT_Strong_Eventual_Consistency/StrongConvergence.thy

View Options

thys/WebAssembly/Wasm_Checker_Types.thy

View Options

thys/WebAssembly/Wasm_Properties.thy

View Options

thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy

View Options

thys/Winding_Number_Eval/Missing_Transcendental.thy

View Options

thys/Winding_Number_Eval/Winding_Number_Eval.thy

View Options

thys/Word_Lib/More_Word_Operations.thy

View Options

thys/Word_Lib/Word_Lemmas.thy

View Options

thys/ZFC_in_HOL/ZFC_in_HOL.thy