Description

Adaptive_State_Counting/

FSM/

FSM_Product.thy

Akra_Bazzi/

akra_bazzi.ML

AnselmGod/

document/

Architectural_Design_Patterns/

document/

EquivalenceOfBicategories.thy

Aristotles_Assertoric_Syllogistic/

AristotlesAssertoric.thy

Attack_Trees/

GDPRhealthcare.thy

MC.thy

Auto2_HOL/

HOL/

Auto2_Imperative_HOL/

Imperative/

assn_matcher.ML

Automatic_Refinement/

Lib/

BTree/

Bicategory/

BicategoryOfSpans.thy

Coherence.thy

ConcreteBicategory.thy

InternalAdjunction.thy

InternalEquivalence.thy

Modification.thy

Prebicategory.thy

Pseudofunctor.thy

PseudonaturalTransformation.thy

document/

Blue_Eyes/

CISC-Kernel/

document/

CZH_ECAT_Structure_Example.thy

CZH_Elementary_Categories/

czh_ecategories/

CZH_ECAT_Comma.thy

CZH_ECAT_Functor.thy

CZH_ECAT_NTCF.thy

CZH_ECAT_PCategory.thy

CZH_ECAT_Rel.thy

CZH_ECAT_Set.thy

CZH_ECAT_Simple.thy

CZH_ECAT_Yoneda.thy

document/

EquivalenceOfCategories.thy

CZH_Foundations/

czh_digraphs/

CZH_DG_DGHM.thy

CZH_DG_Rel.thy

czh_semicategories/

CZH_SMC_Rel.thy

CZH_SMC_Semifunctor.thy

CZH_Universal_Constructions/

czh_ucategories/

Category3/

Functor.thy

FunctorCategory.thy

Limit.thy

NaturalTransformation.thy

SetCat.thy

SetCategory.thy

Yoneda.thy

CoCon/

Traceback_Properties.thy

CoSMeDis/

Post_Confidentiality/

Post_Observation_Setup_RECEIVER.thy

CoSMed/

ROOT

Traceback_Properties/

Post_Visibility_Traceback.thy

Collections/

ICF/

tools/

ICF_Tools.thy

Combinatorics_Words/

document/

Combinatorics_Words_Graph_Lemma/

document/

Combinatorics_Words_Lyndon/

document/

Complete_Non_Orders/

Fixed_Points.thy

Complex_Bounded_Operators/

ROOT

Complex_Geometry/

More_Transcendental.thy

ConcurrentIMP/

document/

Binary_Iterings_Nonstrict.thy

Conditional_Transfer_Rule/

UD/

Constructor_Funs/

Binary_Iterings_Strict.thy

Boolean_Semirings.thy

Capped_Omega_Algebras.thy

General_Refinement_Algebras.thy

Hoare.thy

Hoare_Modal.thy

Lattice_Ordered_Semirings.thy

Monotonic_Boolean_Transformers.thy

Monotonic_Boolean_Transformers_Instances.thy

N_Algebras.thy

N_Omega_Algebras.thy

N_Omega_Binary_Iterings.thy

N_Relation_Algebras.thy

N_Semirings.thy

N_Semirings_Boolean.thy

N_Semirings_Modal.thy

CC_Polynomials_Extra.thy

Count_Circle.thy

Count_Complex_Roots.thy

Count_Complex_Roots_Examples.thy

Cubic_Quartic_Equations/

document/

Delta_System_Lemma/

Design_Theory/

Design_Isomorphisms.thy

Design_Theory_Root.thy

Designs_And_Graphs.thy

Group_Divisible_Designs.thy

Multisets_Extras.thy

Resolvable_Designs.thy

Sub_Designs.thy

Dict_Construction/

transfer_termination.ML

DynamicArchitectures/

document/

EdmondsKarp_Maxflow/

document/

Factored_Transition_System_Bounding/

document/

First_Welfare_Theorem/

document/

Flow_Networks/

document/

Flyspeck-Tame/

FaceDivisionProps.thy

Gabow_SCC/

document/

Finite_Fourier_Series.thy

Gauss_Sums/

Goedel_Incompleteness/

document/

root.tex

Green/

document/

IEEE_Floating_Point/

Conversion_IEEE_Float.thy

IEEE_Properties.thy

IMP2/

lib/

named_simpsets.ML

IMP2_Binary_Heap/

document/

IP_Addresses/

Lib_Word_toString.thy

NumberWang_IPv6.thy

Impossible_Geometry/

Impossible_Geometry.thy

Isabelle_C/

C11-FrontEnd/

src/

C_Lexer_Annotation.thy

Isabelle_Marries_Dirac/

Deutsch.thy

Jacobson_Basic_Algebra/

Group_Theory.thy

JinjaDCI/

BV/

Common/

Compiler/

JVM/

document/

Kuratowski_Closure_Complement/

document/

LOFT/

document/

Lazy_Case/

MiniSail/

ContextSubtypingL.thy

document/

Minsky_Machines/

document/

HNF_Mod_Det_Soundness.thy

Modular_arithmetic_LLL_and_HNF_algorithms/

Storjohann.thy

Monad_Memo_DP/

document/

MonoidalCategory/

MonoidalCategory.thy

Nominal2/

nominal_function_core.ML

Ordinal_Partitions/

Omega_Omega.thy

Partitions.thy

PLM/

TAO_99_SanityTests.thy

document/

Padic_Ints/

document/

Poincare_Disc/

document/

Linear_Algebra_Complements.thy

Projective_Measurements/

CHSH_Inequality.thy

Projective_Measurements.thy

Prpu_Maxflow/

document/

Axioms_Complement_Quantum.thy

ROOTS

Randomised_Social_Choice/

document/

root.tex

Refine_Monadic/

Refine_Automation.thy

document/

Axioms_Complement.thy

Axioms_Quantum.thy

Check_Autogenerated_Files.thy

Classical_Extra.thy

Finite_Tensor_Product.thy

Finite_Tensor_Product_Matrices.thy

Laws_Complement_Quantum.thy

Regression_Test_Selection/

Common/

CollectionBasedRTS.thy

CollectionSemantics.thy

RTS_safe.thy

Semantics.thy

JVM_RTS/

JVMCollectionBasedRTS.thy

JVMCollectionSemantics.thy

JVMSemantics.thy

JinjaSuppl/

ClassesAbove.thy

ClassesChanged.thy

JVMExecStepInductive.thy

Subcls.thy

Saturation_Framework_Extensions/

Standard_Redundancy_Criterion.thy

SpecCheck/

Examples/

SpecCheck_Examples.thy

Output_Styles/

output_style_custom.ML

TESL_Language/

Three_Circles/

document/

Types_Tableaus_and_Goedels_God/

document/

Bit_Shifts_Infix_Syntax.thy

Types_To_Sets_Extension/

ETTS/

Manual/

ETTS_Syntax.thy

Universal_Turing_Machine/

UF.thy

Verified_SAT_Based_AI_Planning/

SAS_Plus_STRIPS.thy

SAT_Plan_Base.thy

STRIPS_Semantics.thy

Vickrey_Clarke_Groves/

Weighted_Path_Order/

Machine_Word_32_Basics.thy

Machine_Word_64.thy

Machine_Word_64_Basics.thy

More_Arithmetic.thy

More_Word.thy

More_Word_Operations.thy

Most_significant_bit.thy

Next_and_Prev.thy

Norm_Words.thy

Reversed_Bit_Lists.thy

Rsplit.thy

Signed_Division_Word.thy

Singleton_Bit_Shifts.thy

SymbolicExecution.thy

X86_InstructionSemantics.thy

Algebraic_Numbers.html

Belief_Revision.html

Bernoulli.html

Bertrands_Postulate.html

Comparison_Sort_Lower_Bound.html

Complete_Non_Orders.html

Complex_Bounded_Operators.html

Correctness_Algebras.html

Count_Complex_Roots.html

Density_Compiler.html

Descartes_Sign_Rule.html

Dirichlet_L.html

Dirichlet_Series.html

E_Transcendental.html

Ergodic_Theory.html

Error_Function.html

Euler_MacLaurin.html

Finitely_Generated_Abelian_Groups.html

Fishburn_Impossibility.html

Fisher_Yates.html

Formal_Puiseux_Series.html

Furstenberg_Topology.html

Gauss_Sums.html

Gaussian_Integers.html

Green.html

Hermite_Lindemann.html

IMO2019.html

Lambert_W.html

Landau_Symbols.html

Laws_of_Large_Numbers.html

Linear_Recurrences.html

Liouville_Numbers.html

List_Inversions.html

MFODL_Monitor_Optimized.html

Mason_Stothers.html

Median_Of_Medians_Selection.html

Mersenne_Primes.html

Minkowskis_Theorem.html

Monad_Normalisation.html

MonoBoolTranAlgebra.html

Myhill-Nerode.html

Pell.html

Pi_Transcendental.html

Polynomial_Interpolation.html

Power_Sum_Polynomials.html

Prime_Distribution_Elementary.html

Prime_Harmonic_Series.html

Prime_Number_Theorem.html

Probabilistic_Prime_Tests.html

Quick_Sort_Cost.html

Random_BSTs.html

Randomised_BSTs.html

Randomised_Social_Choice.html

Registers.html

Regular-Sets.html

SDS_Impossibility.html

Skip_Lists.html

Stirling_Formula.html

Stone_Kleene_Relation_Algebras.html

Sturm_Sequences.html

Subset_Boolean_Algebras.html

Symmetric_Polynomials.html

Zeta_3_Irrational.html

rAFP4f170b69e2da

metadata/metadata

metadata/templates/about.tpl

thys/AI_Planning_Languages_Semantics/document/root.bib

thys/Adaptive_State_Counting/FSM/FSM_Product.thy

thys/Akra_Bazzi/akra_bazzi.ML

thys/AnselmGod/document/root.bib

thys/Architectural_Design_Patterns/document/root.bib

thys/Aristotles_Assertoric_Syllogistic/AristotlesAssertoric.thy

thys/Attack_Trees/GDPRhealthcare.thy

thys/Attack_Trees/MC.thy

thys/Auto2_HOL/HOL/order.ML

thys/Auto2_HOL/consts.ML

thys/Auto2_HOL/items.ML

thys/Auto2_HOL/logic_steps.ML

thys/Auto2_HOL/normalize.ML

thys/Auto2_HOL/status.ML

thys/Auto2_HOL/util.ML

thys/Auto2_Imperative_HOL/Imperative/assn_matcher.ML

thys/Automatic_Refinement/Lib/Mk_Term_Antiquot.thy

thys/Automatic_Refinement/Lib/Mpat_Antiquot.thy

thys/Automatic_Refinement/Lib/Refine_Util.thy

thys/BTree/ROOT

thys/Belief_Revision/AGM_Contraction.thy

thys/Belief_Revision/AGM_Logic.thy

thys/Belief_Revision/AGM_Remainder.thy

thys/Belief_Revision/AGM_Revision.thy

thys/Belief_Revision/ROOT

thys/Belief_Revision/document/adb-long.bib

thys/Belief_Revision/document/graph_locales.pdf

thys/Belief_Revision/document/root.bib

thys/Belief_Revision/document/root.tex

thys/Bicategory/Bicategory.thy

thys/Bicategory/BicategoryOfSpans.thy

thys/Bicategory/Coherence.thy

thys/Bicategory/ConcreteBicategory.thy

thys/Bicategory/EquivalenceOfBicategories.thy

thys/Bicategory/InternalAdjunction.thy

thys/Bicategory/InternalEquivalence.thy

thys/Bicategory/Modification.thy

thys/Bicategory/Prebicategory.thy

thys/Bicategory/Pseudofunctor.thy

thys/Bicategory/PseudonaturalTransformation.thy

thys/Bicategory/SpanBicategory.thy

thys/Bicategory/Strictness.thy

thys/Bicategory/Subbicategory.thy

thys/Bicategory/Tabulation.thy

thys/Bicategory/document/root.tex

thys/Blue_Eyes/Blue_Eyes.thy

thys/CISC-Kernel/document/root.bib

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Comma.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Functor.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_NTCF.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_PCategory.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Rel.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Set.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Simple.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Structure_Example.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Yoneda.thy

thys/CZH_Elementary_Categories/document/root.bib

thys/CZH_Foundations/czh_digraphs/CZH_DG_DGHM.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Rel.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Rel.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semifunctor.thy

thys/CZH_Universal_Constructions/ROOT

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Kan.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan.thy

thys/Category3/BinaryFunctor.thy

thys/Category3/Category.thy

thys/Category3/EquivalenceOfCategories.thy

thys/Category3/Functor.thy

thys/Category3/FunctorCategory.thy

thys/Category3/Limit.thy

thys/Category3/NaturalTransformation.thy

thys/Category3/SetCat.thy

thys/Category3/SetCategory.thy

thys/Category3/Yoneda.thy

thys/CoCon/Traceback_Properties.thy

thys/CoSMeDis/Post_Confidentiality/Post_Observation_Setup_RECEIVER.thy

thys/CoSMed/ROOT

thys/CoSMed/Traceback_Properties/Post_Visibility_Traceback.thy

thys/Collections/ICF/tools/ICF_Tools.thy

thys/Combinatorics_Words/document/root.bib

thys/Combinatorics_Words_Graph_Lemma/document/root.bib

thys/Combinatorics_Words_Lyndon/document/root.bib

thys/Complete_Non_Orders/Fixed_Points.thy

thys/Complex_Bounded_Operators/ROOT

thys/Complex_Geometry/More_Transcendental.thy

thys/ConcurrentIMP/document/root.bib

thys/Conditional_Transfer_Rule/UD/UD.ML

thys/Conditional_Transfer_Rule/UD/UD_Reference.thy

thys/Constructor_Funs/constructor_funs.ML

thys/Correctness_Algebras/Approximation.thy

thys/Correctness_Algebras/Base.thy

thys/Correctness_Algebras/Binary_Iterings.thy

thys/Correctness_Algebras/Binary_Iterings_Nonstrict.thy

thys/Correctness_Algebras/Binary_Iterings_Strict.thy

thys/Correctness_Algebras/Boolean_Semirings.thy

thys/Correctness_Algebras/Capped_Omega_Algebras.thy

thys/Correctness_Algebras/Complete_Domain.thy

thys/Correctness_Algebras/Complete_Tests.thy

thys/Correctness_Algebras/Domain.thy

thys/Correctness_Algebras/Domain_Iterings.thy

thys/Correctness_Algebras/Domain_Recursion.thy

thys/Correctness_Algebras/Extended_Designs.thy

thys/Correctness_Algebras/General_Refinement_Algebras.thy

thys/Correctness_Algebras/Hoare.thy

thys/Correctness_Algebras/Hoare_Modal.thy

thys/Correctness_Algebras/Lattice_Ordered_Semirings.thy

thys/Correctness_Algebras/Monotonic_Boolean_Transformers.thy

thys/Correctness_Algebras/Monotonic_Boolean_Transformers_Instances.thy

thys/Correctness_Algebras/N_Algebras.thy

thys/Correctness_Algebras/N_Omega_Algebras.thy

thys/Correctness_Algebras/N_Omega_Binary_Iterings.thy

thys/Correctness_Algebras/N_Relation_Algebras.thy

thys/Correctness_Algebras/N_Semirings.thy

thys/Correctness_Algebras/N_Semirings_Boolean.thy

thys/Correctness_Algebras/N_Semirings_Modal.thy

thys/Correctness_Algebras/Omega_Algebras.thy

thys/Correctness_Algebras/Pre_Post.thy

thys/Correctness_Algebras/Pre_Post_Modal.thy

thys/Correctness_Algebras/Preconditions.thy

thys/Correctness_Algebras/ROOT

thys/Correctness_Algebras/Recursion.thy

thys/Correctness_Algebras/Recursion_Strict.thy

thys/Correctness_Algebras/Relative_Domain.thy

thys/Correctness_Algebras/Relative_Modal.thy

thys/Correctness_Algebras/Test_Iterings.thy

thys/Correctness_Algebras/Tests.thy

thys/Correctness_Algebras/document/root.bib

thys/Correctness_Algebras/document/root.tex

thys/Count_Complex_Roots/CC_Polynomials_Extra.thy

thys/Count_Complex_Roots/Count_Circle.thy

thys/Count_Complex_Roots/Count_Complex_Roots.thy

thys/Count_Complex_Roots/Count_Complex_Roots_Examples.thy

thys/Count_Complex_Roots/Count_Half_Plane.thy

thys/Count_Complex_Roots/Count_Line.thy

thys/Count_Complex_Roots/Count_Rectangle.thy

thys/Count_Complex_Roots/Extended_Sturm.thy

thys/Count_Complex_Roots/More_Polynomials.thy

thys/Count_Complex_Roots/ROOT

thys/Cubic_Quartic_Equations/document/root.tex

thys/Delta_System_Lemma/Cardinal_Library.thy

thys/Delta_System_Lemma/Cofinality.thy

thys/Design_Theory/BIBD.thy

thys/Design_Theory/Block_Designs.thy

thys/Design_Theory/Design_Basics.thy

thys/Design_Theory/Design_Isomorphisms.thy

thys/Design_Theory/Design_Theory_Root.thy

thys/Design_Theory/Designs_And_Graphs.thy

thys/Design_Theory/Group_Divisible_Designs.thy

thys/Design_Theory/Multisets_Extras.thy

thys/Design_Theory/Resolvable_Designs.thy

thys/Design_Theory/Sub_Designs.thy

thys/Dict_Construction/transfer_termination.ML

thys/DynamicArchitectures/document/root.bib

thys/EdmondsKarp_Maxflow/document/root.bib

thys/Factored_Transition_System_Bounding/document/root.bib

thys/First_Welfare_Theorem/document/root.bib

thys/Flow_Networks/document/root.bib

thys/Flyspeck-Tame/FaceDivisionProps.thy

thys/Gabow_SCC/document/root.bib

thys/Gauss_Sums/Finite_Fourier_Series.thy

thys/Goedel_Incompleteness/document/root.tex

thys/Green/document/root.tex

thys/Huffman/ROOT

thys/Huffman/document/preprocessor

thys/IEEE_Floating_Point/Conversion_IEEE_Float.thy

thys/IEEE_Floating_Point/IEEE_Properties.thy

thys/IMP2/lib/named_simpsets.ML

thys/IMP2_Binary_Heap/document/root.bib

thys/IMP2_Binary_Heap/document/root.tex

thys/IP_Addresses/IP_Address.thy

thys/IP_Addresses/IPv4.thy

thys/IP_Addresses/IPv6.thy

thys/IP_Addresses/Lib_Word_toString.thy

thys/IP_Addresses/NumberWang_IPv6.thy

thys/Impossible_Geometry/Impossible_Geometry.thy

thys/Isabelle_C/C11-FrontEnd/src/C_Lexer_Annotation.thy

thys/Isabelle_Marries_Dirac/Deutsch.thy

thys/Jacobson_Basic_Algebra/Group_Theory.thy

thys/JinjaDCI/BV/BVConform.thy

thys/JinjaDCI/BV/BVExec.thy

thys/JinjaDCI/BV/BVNoTypeError.thy

thys/JinjaDCI/BV/BVSpec.thy

thys/JinjaDCI/BV/BVSpecTypeSafe.thy

thys/JinjaDCI/BV/ClassAdd.thy

thys/JinjaDCI/BV/Effect.thy

thys/JinjaDCI/BV/EffectMono.thy

thys/JinjaDCI/BV/JVM_SemiType.thy

thys/JinjaDCI/BV/LBVJVM.thy

thys/JinjaDCI/BV/SemiType.thy

thys/JinjaDCI/BV/TF_JVM.thy

thys/JinjaDCI/Common/Auxiliary.thy

thys/JinjaDCI/Common/Conform.thy

thys/JinjaDCI/Common/Decl.thy

thys/JinjaDCI/Common/Exceptions.thy

thys/JinjaDCI/Common/Objects.thy

thys/JinjaDCI/Common/SystemClasses.thy

thys/JinjaDCI/Common/Type.thy

thys/JinjaDCI/Common/TypeRel.thy

thys/JinjaDCI/Common/Value.thy

thys/JinjaDCI/Common/WellForm.thy

thys/JinjaDCI/Compiler/Compiler.thy

thys/JinjaDCI/Compiler/Compiler1.thy

thys/JinjaDCI/Compiler/Compiler2.thy

thys/JinjaDCI/Compiler/Correctness1.thy

thys/JinjaDCI/Compiler/Correctness2.thy

thys/JinjaDCI/Compiler/Hidden.thy

thys/JinjaDCI/Compiler/J1.thy

thys/JinjaDCI/Compiler/J1WellForm.thy

thys/JinjaDCI/Compiler/PCompiler.thy

thys/JinjaDCI/Compiler/TypeComp.thy

thys/JinjaDCI/J/Annotate.thy

thys/JinjaDCI/J/BigStep.thy

thys/JinjaDCI/J/DefAss.thy

thys/JinjaDCI/J/EConform.thy

thys/JinjaDCI/J/Equivalence.thy

thys/JinjaDCI/J/Expr.thy

thys/JinjaDCI/J/JWellForm.thy

thys/JinjaDCI/J/Progress.thy

thys/JinjaDCI/J/SmallStep.thy

thys/JinjaDCI/J/State.thy

thys/JinjaDCI/J/TypeSafe.thy

thys/JinjaDCI/J/WWellForm.thy

thys/JinjaDCI/J/WellType.thy

thys/JinjaDCI/J/WellTypeRT.thy

thys/JinjaDCI/JVM/JVMDefensive.thy

thys/JinjaDCI/JVM/JVMExceptions.thy

thys/JinjaDCI/JVM/JVMExec.thy

thys/JinjaDCI/JVM/JVMExecInstr.thy

thys/JinjaDCI/JVM/JVMInstructions.thy

thys/JinjaDCI/JVM/JVMState.thy

thys/JinjaDCI/JinjaDCI.thy

thys/JinjaDCI/document/root.bib

thys/Kuratowski_Closure_Complement/document/root.bib

thys/LOFT/document/chap3.tex

thys/LOFT/document/root.tex

thys/Lazy_Case/lazy_case.ML

thys/MiniSail/BTVSubst.thy

thys/MiniSail/BTVSubstTypingL.thy

thys/MiniSail/ContextSubtypingL.thy

thys/MiniSail/IVSubst.thy

thys/MiniSail/IVSubstTypingL.thy

thys/MiniSail/MiniSail.thy

thys/MiniSail/Nominal-Utils.thy

thys/MiniSail/Operational.thy

thys/MiniSail/RCLogic.thy

thys/MiniSail/RCLogicL.thy

thys/MiniSail/ROOT

thys/MiniSail/Safety.thy

thys/MiniSail/SubstMethods.thy

thys/MiniSail/Syntax.thy

thys/MiniSail/SyntaxL.thy

thys/MiniSail/Typing.thy

thys/MiniSail/TypingL.thy

thys/MiniSail/Wellformed.thy

thys/MiniSail/WellformedL.thy

thys/MiniSail/document/root.tex

thys/Minsky_Machines/document/root.bib

thys/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Storjohann.thy

thys/Monad_Memo_DP/document/root.bib

thys/MonoidalCategory/MonoidalCategory.thy

thys/Nominal2/nominal_function_core.ML

thys/Ordinal_Partitions/Omega_Omega.thy

thys/Ordinal_Partitions/Partitions.thy

thys/PLM/TAO_99_SanityTests.thy

thys/PLM/document/root.bib

thys/Padic_Ints/document/root.bib

thys/Poincare_Disc/document/root.bib

thys/Projective_Measurements/CHSH_Inequality.thy

thys/Projective_Measurements/Linear_Algebra_Complements.thy

thys/Projective_Measurements/Projective_Measurements.thy

thys/Prpu_Maxflow/document/root.bib

thys/ROOTS

thys/Randomised_Social_Choice/document/root.tex

thys/Refine_Monadic/Refine_Automation.thy

thys/Refine_Monadic/document/root.bib

thys/Registers/Axioms.thy

thys/Registers/Axioms_Classical.thy

thys/Registers/Axioms_Complement.thy

thys/Registers/Axioms_Complement_Quantum.thy

thys/Registers/Axioms_Quantum.thy

thys/Registers/Check_Autogenerated_Files.thy

thys/Registers/Classical_Extra.thy

thys/Registers/Finite_Tensor_Product.thy

thys/Registers/Finite_Tensor_Product_Matrices.thy

thys/Registers/LICENSE

thys/Registers/Laws.thy

thys/Registers/Laws_Classical.thy

thys/Registers/Laws_Complement.thy

thys/Registers/Laws_Complement_Quantum.thy

thys/Registers/Laws_Quantum.thy

thys/Registers/Misc.thy

thys/Registers/Pure_States.thy

thys/Registers/QHoare.thy

thys/Registers/Quantum.thy

thys/Registers/Quantum_Extra.thy

thys/Registers/Quantum_Extra2.thy

thys/Registers/ROOT

thys/Registers/Teleport.thy

thys/Registers/document/root.bib

thys/Registers/document/root.tex

thys/Registers/instantiate_laws.py

thys/Regression_Test_Selection/Common/CollectionBasedRTS.thy

thys/Regression_Test_Selection/Common/CollectionSemantics.thy

thys/Regression_Test_Selection/Common/RTS_safe.thy

thys/Regression_Test_Selection/Common/Semantics.thy

thys/Regression_Test_Selection/JVM_RTS/JVMCollectionBasedRTS.thy

thys/Regression_Test_Selection/JVM_RTS/JVMCollectionSemantics.thy

thys/Regression_Test_Selection/JVM_RTS/JVMSemantics.thy

thys/Regression_Test_Selection/JinjaSuppl/ClassesAbove.thy

thys/Regression_Test_Selection/JinjaSuppl/ClassesChanged.thy

thys/Regression_Test_Selection/JinjaSuppl/JVMExecStepInductive.thy

thys/Regression_Test_Selection/JinjaSuppl/Subcls.thy

thys/Saturation_Framework_Extensions/Standard_Redundancy_Criterion.thy

thys/SpecCheck/Examples/SpecCheck_Examples.thy

thys/SpecCheck/Output_Styles/output_style_custom.ML

thys/SpecCheck/README.md

thys/SpecCheck/property.ML

thys/SpecCheck/speccheck.ML

thys/TESL_Language/Introduction.thy

thys/Three_Circles/Bernstein.thy

thys/Three_Circles/Bernstein_01.thy

thys/Three_Circles/Normal_Poly.thy

thys/Three_Circles/ROOT

thys/Three_Circles/RRI_Misc.thy

thys/Three_Circles/Three_Circles.thy

thys/Three_Circles/document/root.bib

thys/Three_Circles/document/root.tex

thys/Types_Tableaus_and_Goedels_God/document/root.bib

thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Syntax.thy

thys/Universal_Turing_Machine/UF.thy

thys/Verified_SAT_Based_AI_Planning/SAS_Plus_STRIPS.thy

thys/Verified_SAT_Based_AI_Planning/SAT_Plan_Base.thy

thys/Verified_SAT_Based_AI_Planning/STRIPS_Semantics.thy

thys/Vickrey_Clarke_Groves/MiscTools.thy

thys/Weighted_Path_Order/KBO_as_WPO.thy

thys/Word_Lib/Aligned.thy

thys/Word_Lib/Bit_Shifts_Infix_Syntax.thy

thys/Word_Lib/Bits_Int.thy

thys/Word_Lib/Bitwise.thy

thys/Word_Lib/Examples.thy

thys/Word_Lib/Generic_set_bit.thy

thys/Word_Lib/Guide.thy

thys/Word_Lib/Machine_Word_32.thy

thys/Word_Lib/Machine_Word_32_Basics.thy

thys/Word_Lib/Machine_Word_64.thy

thys/Word_Lib/Machine_Word_64_Basics.thy

thys/Word_Lib/More_Arithmetic.thy

thys/Word_Lib/More_Word.thy

thys/Word_Lib/More_Word_Operations.thy

thys/Word_Lib/Most_significant_bit.thy

thys/Word_Lib/Next_and_Prev.thy

thys/Word_Lib/Norm_Words.thy

thys/Word_Lib/Reversed_Bit_Lists.thy

thys/Word_Lib/Rsplit.thy

thys/Word_Lib/Signed_Division_Word.thy

thys/Word_Lib/Singleton_Bit_Shifts.thy

thys/Word_Lib/Word_32.thy

thys/Word_Lib/Word_64.thy

thys/Word_Lib/Word_EqI.thy

thys/Word_Lib/Word_Lemmas.thy

thys/Word_Lib/Word_Lib_Sumo.thy

thys/X86_Semantics/BitByte.thy

thys/X86_Semantics/Example_WC.thy

thys/X86_Semantics/Examples.thy

thys/X86_Semantics/Memory.thy

thys/X86_Semantics/MySubst.ML

thys/X86_Semantics/README

thys/X86_Semantics/ROOT

thys/X86_Semantics/State.thy

thys/X86_Semantics/StateCleanUp.thy

thys/X86_Semantics/SymbolicExecution.thy

thys/X86_Semantics/X86_InstructionSemantics.thy

thys/X86_Semantics/X86_Parse.ML

thys/X86_Semantics/X86_Parse.thy

thys/X86_Semantics/document/root.bib

thys/X86_Semantics/document/root.tex

web/about.html

web/entries/Akra_Bazzi.html

web/entries/Algebraic_Numbers.html

web/entries/Belief_Revision.html

web/entries/Bernoulli.html

web/entries/Bertrands_Postulate.html

web/entries/Bicategory.html

web/entries/Buffons_Needle.html

web/entries/CISC-Kernel.html

web/entries/Catalan_Numbers.html

web/entries/Category3.html

web/entries/Comparison_Sort_Lower_Bound.html

web/entries/Complete_Non_Orders.html

web/entries/Complex_Bounded_Operators.html

web/entries/Correctness_Algebras.html

web/entries/Count_Complex_Roots.html

web/entries/Density_Compiler.html

web/entries/Descartes_Sign_Rule.html

web/entries/Dirichlet_L.html

web/entries/Dirichlet_Series.html

web/entries/E_Transcendental.html

web/entries/Ergodic_Theory.html

web/entries/Error_Function.html

web/entries/Euler_MacLaurin.html

web/entries/Finitely_Generated_Abelian_Groups.html

web/entries/Fishburn_Impossibility.html

web/entries/Fisher_Yates.html

web/entries/Formal_Puiseux_Series.html

web/entries/Furstenberg_Topology.html

web/entries/Gauss_Sums.html

web/entries/Gaussian_Integers.html

web/entries/Green.html

web/entries/Hermite_Lindemann.html

web/entries/IMO2019.html

web/entries/Lambert_W.html

web/entries/Landau_Symbols.html

web/entries/Laws_of_Large_Numbers.html

web/entries/Linear_Recurrences.html

web/entries/Liouville_Numbers.html

web/entries/List_Inversions.html

web/entries/MFODL_Monitor_Optimized.html

web/entries/Mason_Stothers.html

web/entries/Median_Of_Medians_Selection.html

web/entries/Mersenne_Primes.html

web/entries/Minkowskis_Theorem.html

web/entries/Monad_Normalisation.html

web/entries/MonoBoolTranAlgebra.html

web/entries/Myhill-Nerode.html

web/entries/Pell.html

web/entries/Pi_Transcendental.html

web/entries/Polynomial_Interpolation.html

web/entries/Power_Sum_Polynomials.html

web/entries/Prime_Distribution_Elementary.html

web/entries/Prime_Harmonic_Series.html

web/entries/Prime_Number_Theorem.html

web/entries/Probabilistic_Prime_Tests.html

web/entries/Quick_Sort_Cost.html

web/entries/Random_BSTs.html

web/entries/Randomised_BSTs.html

web/entries/Randomised_Social_Choice.html

web/entries/Registers.html

web/entries/Regular-Sets.html

web/entries/SDS_Impossibility.html

web/entries/Skip_Lists.html

web/entries/Stirling_Formula.html

web/entries/Stone_Kleene_Relation_Algebras.html

web/entries/Sturm_Sequences.html

web/entries/Subset_Boolean_Algebras.html

web/entries/Symmetric_Polynomials.html

web/entries/Treaps.html

web/entries/Triangle.html

web/entries/Van_der_Waerden.html

web/entries/Word_Lib.html

web/entries/X86_Semantics.html

web/entries/Zeta_3_Irrational.html

web/entries/Zeta_Function.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html