Description

Finite_Field_Record_Based.thy

Berlekamp_Zassenhaus/

Bicategory/

Bicategory.thy

BicategoryOfSpans.thy

Coherence.thy

EquivalenceOfBicategories.thy

Blue_Eyes/

Bounded_Deducibility_Security/

Buffons_Needle/

Buildings/

CZH_Elementary_Categories

CZH_ECAT_CSimplicial.thy

CZH_ECAT_Category.thy

CZH_ECAT_Comma.thy

CZH_ECAT_Conclusions.thy

CZH_ECAT_Cone.thy

CZH_ECAT_Discrete.thy

CZH_ECAT_Introduction.thy

CZH_ECAT_NTCF.thy

CZH_ECAT_Order.thy

CZH_ECAT_Ordinal.thy

CZH_ECAT_PCategory.thy

CZH_ECAT_Par.thy

CZH_ECAT_Parallel.thy

CZH_ECAT_Small_Category.thy

CZH_ECAT_Small_Cone.thy

CZH_ECAT_Small_Functor.thy

CZH_ECAT_Small_NTCF.thy

CZH_ECAT_Structure_Example.thy

CZH_ECAT_Subcategory.thy

CZH_Foundations/

czh_digraphs/

CZH_DG_Introduction.thy

CZH_DG_Small_DGHM.thy

CZH_DG_Small_Digraph.thy

CZH_DG_Small_TDGHM.thy

CZH_DG_Subdigraph.thy

czh_introduction/

czh_semicategories/

CZH_SMC_PSemicategory.thy

CZH_SMC_Par.thy

CZH_SMC_Rel.thy

CZH_SMC_SemiCAT.thy

CZH_SMC_Semicategory.thy

CZH_SMC_Semifunctor.thy

CZH_SMC_Set.thy

CZH_SMC_Simple.thy

CZH_SMC_Small_NTSMCF.thy

CZH_SMC_Small_Semicategory.thy

CZH_SMC_Small_Semifunctor.thy

CZH_SMC_Subsemicategory.thy

czh_sets/

CZH_Sets_BRelations.thy

CZH_Sets_FBRelations.thy

CZH_Sets_FSequences.thy

CZH_Sets_IF.thy

CZH_Sets_Introduction.thy

ex/

document/

CZH_Universal_Constructions

czh_ucategories

CZH_UCAT_Adjoints.thy

CZH_UCAT_Comma.thy

CZH_UCAT_Complete.thy

CZH_UCAT_Conclusions.thy

CZH_UCAT_Kan.thy

CZH_UCAT_Limit.thy

CZH_UCAT_Limit_Equalizer.thy

CZH_UCAT_Limit_IT.thy

CZH_UCAT_Limit_Product.thy

CZH_UCAT_Limit_Pullback.thy

CZH_UCAT_PWKan.thy

CZH_UCAT_PWKan_Example.thy

CZH_UCAT_Pointed.thy

CZH_UCAT_Representable.thy

CZH_UCAT_Set.thy

CZH_UCAT_Universal.thy

document/

root.bib

CakeML/

Tools/

cakeml_compiler.ML

Catalan_Numbers/

Catalan_Auxiliary_Integral.thy

Catalan_Numbers.thy

Category3

Adjunction.thy

EquivalenceOfCategories.thy

Clique_and_Monotone_Circuits/

Assumptions_and_Approximations.thy

Clique_Large_Monotone_Circuits.thy

Collections/

Examples/

Autoref/

Simple_DFS.thy

GenCF/

Impl/

Impl_Bit_Set.thy

Lib/

Code_Target_ICF.thy

Completeness/

PermutationLemmas.thy

Sequents.thy

Complex_Bounded_Operators

Cblinfun_Code.thy

Cblinfun_Code_Examples.thy

Complex_Bounded_Linear_Function.thy

Complex_L2.thy

Complex_Vector_Spaces.thy

One_Dimensional_Spaces.thy

Complx/

ex/

Conditional_Simplification/

Core_DOM/

standard/

Core_DOM_Heap_WF.thy

Core_SC_DOM/

safely_composable/

Core_DOM_Heap_WF.thy

Differential_Dynamic_Logic/

document/

root.bib

Dirichlet_L/

Dirichlet_L_Functions.thy

Dirichlet_Series/

Dirichlet_Series_Analysis.thy

DiscretePricing/

Disc_Cond_Expect.thy

Fair_Price.thy

Dominance_CHK/

Cfg.thy

Dom_Kildall_Property.thy

DynamicArchitectures/

Configuration_Traces.thy

Dynamic_Tables/

Epistemic_Logic/

Ergodic_Theory/

Error_Function/

Error_Function_Asymptotics.thy

Euler_MacLaurin/

Euler_MacLaurin.thy

Extended_Finite_State_Machines/

EFSM_LTL.thy

examples/

Drinks_Machine_LTL.thy

FOL_Axiomatic

FOL_Axiomatic.thy

FOL_Axiomatic_Variant.thy

FO_Theory_Rewriting/

Card_Irreducible_Polynomials_Aux.thy

Util/

Multihole_Context.thy

Factor_Algebraic_Polynomial/

MPoly_Divide.thy

Finite_Fields/

Flow_Networks/

Residual_Graph.thy

Foundation_of_geometry/

document/

Fourier/

Frequency_Moments/

Frequency_Moment_0.thy

Frequency_Moment_2.thy

Frequency_Moment_k.thy

Frequency_Moments_Preliminary_Results.thy

Functional_Ordered_Resolution_Prover/

IsaFoR_Term.thy

Gale_Shapley/

Gale_Shapley1.thy

Gale_Shapley2.thy

Game_Based_Crypto/

CryptHOL_Tutorial.thy

Girth_Chromatic/

Ugraphs.thy

Goedel_HFSet_Semanticless/

Sigma.thy

Graph_Theory/

Digraph_Isomorphism.thy

Green/

Groebner_Macaulay/

Cone_Decomposition.thy

Dube_Bound.thy

Dube_Prelims.thy

Grothendieck_Schemes/

Comm_Ring.thy

Scheme.thy

Hidden_Markov_Models/

Hidden_Markov_Model.thy

Hoare_Time/

Big_StepT_Partial.thy

IEEE_Floating_Point/

IP_Addresses/

Incompleteness/

Inductive_Inference/

Partial_Recursive.thy

Universal.thy

Interpolation_Polynomials_HOL_Algebra/

Bounded_Degree_Polynomials.thy

Interpolation_Polynomial_Cardinalities.thy

Lagrange_Interpolation.thy

Interval_Arithmetic_Word32/

Finite_String.thy

Interpreter.thy

Iptables_Semantics/

Primitive_Matchers/

Code_Interface.thy

IpAddresses.thy

Irrationals_From_THEBOOK/

Irrationals_From_THEBOOK.thy

document/

	appendices/

document/

generated/

c_grammar_fun.grm.sig

main

	main/

src/

C_Lexer_Annotation.thy

C_Lexer_Language.thy

C_Parser_Annotation.thy

C_Parser_Language.thy

README.thy

MFMC_Flow_Attainability.thy

Isabelle_Meta_Model/

isabelle_home/

src/

Tools/

Code/

Isabelle_code_target.thy

JinjaThreads/

Basic/

Common/

Compiler/

Execute/

Framework/

MM/

Jordan_Normal_Form/

Lambert_W/

Laplace_Transform/

Lifting_the_Exponent/

List_Update/

Lp/

Functional_Spaces.thy

MDP-Rewards/

MDP_disc.thy

MFMC_Countable/

MFMC_Unbounded.thy

MFMC_Web.thy

Markov_Models/

Continuous_Time_Markov_Chain.thy

ex/

Mereology/

Mersenne_Primes/

Lucas_Lehmer_Code.thy

MonoidalCategory/

FreeMonoidalCategory.thy

Nash_Williams/

Nash_Williams.thy

Native_Word

Bits_Integer.thy

Code_Int_Integer_Conversion.thy

Code_Symbolic_Bits_Int.thy

	Code_Symbolic_Int_Bit.thy
	Code_Symbolic_Bits_Int.thy

Code_Target_Bits_Int.thy

	Code_Target_Int_Bit.thy
	Code_Target_Bits_Int.thy

	Code_Target_Integer_Bit.thy
	Bits_Integer.thy

Code_Target_Word_Base.thy

Native_Word_Test_Emu.thy

Nested_Multisets_Ordinals/

Multiset_More.thy

Optics/

Lens_Record.ML

Ordered_Resolution_Prover/

Abstract_Substitution.thy

FO_Ordered_Resolution.thy

Ordinal_Partitions/

Partitions.thy

Ordinary_Differential_Equations/

Ex/

Lorenz/

Lorenz_Approximation.thy

IVP/

Cones.thy

Flow.thy

Flow_Congs.thy

Picard_Lindeloef_Qualitative.thy

Poincare_Map.thy

Upper_Lower_Solution.thy

Library/

Gronwall.thy

Linear_ODE.thy

Vector_Derivative_On.thy

Numerics/

Concrete_Reachability_Analysis.thy

Concrete_Reachability_Analysis_C1.thy

Concrete_Rigorous_Numerics.thy

Example_Utilities.thy

Init_ODE_Solver.thy

Refine_Reachability_Analysis.thy

Refine_Reachability_Analysis_C1.thy

Refine_Rigorous_Numerics_Aform.thy

Transfer_Euclidean_Space_Vector.thy

ODE_Auxiliarities.thy

Refinement/

Refine_Vector_List.thy

Weak_Set.thy

PAC_Checker/

PAC_More_Poly.thy

Planarity_Certificates/

Planarity/

Graph_Genus.thy

Poincare_Bendixson/

Analysis_Misc.thy

ODE_Misc.thy

Poincare_Bendixson.thy

Polynomials/

document/

Prefix_Free_Code_Combinators/

Examples.thy

Prefix_Free_Code_Combinators.thy

Prime_Distribution_Elementary/

Moebius_Mu_Sum.thy

Partial_Zeta_Bounds.thy

Prime_Number_Theorem/

Mertens_Theorems.thy

Newman_Ingham_Tauberian.thy

Prime_Counting_Functions.thy

Prime_Number_Theorem.thy

Prime_Number_Theorem_Library.thy

Proof_Strategy_Language/

Subtool.ML

Public_Announcement_Logic/

PAL.thy

document/

Pair_QuasiBorel_Measure.thy

QHLProver/

Complex_Matrix.thy

Quasi_Borel_Spaces/

Probability_Space_QuasiBorel.thy

ROOTS

Random_BSTs/

Random_BSTs.thy

Random_Graph_Subgraph_Threshold/

Ugraph_Lemmas.thy

Real_Power/

Log.thy

RealPower.thy

Refine_Imperative_HOL/

IICF/

Impl/

Heaps/

IICF_Abs_Heap.thy

IICF_Abs_Heapmap.thy

Lib/

Named_Theorems_Rev.thy

Registers/

document/

Regular-Sets/

Rep_Fin_Groups/

Roth_Arithmetic_Progressions/

Roth_Arithmetic_Progressions.thy

document/

Core_DOM_SC_DOM_Components.thy

SC_DOM_Components/

Safe_Distance/

Safe_Distance.thy

Safe_Distance_Reaction.thy

Saturation_Framework/

Given_Clause_Architectures.thy

Saturation_Framework_Extensions/

Clausal_Calculus.thy

Standard_Redundancy_Criterion.thy

Schutz_Spacetime/

TemporalOrderOnPath.thy

Security_Protocol_Refinement/

Refinement/

Message.thy

Signature_Groebner/

Prelims.thy

Smith_Normal_Form

Alternative_Proofs.thy

Smooth_Manifolds/

Sophomores_Dream/

Special_Function_Bounds/

Labeled_Stateful_Strands.thy

Stateful_Protocol_Composition_and_Typing/

Examples.thy

Intruder_Deduction.thy

Parallel_Compositionality.thy

Stateful_Compositionality.thy

Stateful_Strands.thy

Stateful_Typing.thy

Strands_and_Constraints.thy

Typed_Model.thy

Typing_Result.thy

document/

examples/

Example_Keyserver.thy

Example_TLS.thy

Stirling_Formula/

Gamma_Asymptotics.thy

Stirling_Formula.thy

Store_Buffer_Reduction/

SyntaxTweaks.thy

Sturm_Sequences/

Sturm_Method.thy

Sunflowers/

Erdos_Rado_Sunflower.thy

document/

root.bib

Szemeredi_Regularity/

Szemeredi.thy

document/

SML_Topological_Space.thy

Taylor_Models/

Taylor_Models.thy

Types_To_Sets_Extension/

Examples/

SML_Relativization/

Topology/

SML_Product_Topology.thy

UpDown_Scheme/

Triangular_Function.thy

VYDRA_MDL

Interval.thy

Metric_Point_Structure.thy

Timestamp_Lex_Total.thy

document/

Van_Emde_Boas_Trees/

VerifyThis2019/

Virtual_Substitution/

Debruijn.thy

EliminateVariable.thy

ExecutiblePolyProps.thy

OptimizationProofs.thy

WOOT_Strong_Eventual_Consistency/

Consistency.thy

CreateConsistent.thy

DistributedExecution.thy

IntegrateAlgorithm.thy

IntegrateInsertCommute.thy

Psi.thy

SortKeys.thy

WebAssembly/

Wasm_Printing/

Wasm_Interpreter_Printing_Pure.thy

Weight_Balanced_Trees/

Weight_Balanced_Trees_log.thy

Weighted_Path_Order/

Wetzels_Problem/

Bit_Comprehension.thy

Bits_Int.thy

Generic_set_bit.thy

Guide.thy

Least_significant_bit.thy

Many_More.thy

More_Word.thy

More_Word_Operations.thy

Reversed_Bit_Lists.thy

Word_Lemmas.thy

X86_Semantics/

X86_Parse.ML

Youngs_Inequality/

document/

Abstract-Hoare-Logics.html

ZFC_in_HOL

General_Cardinals.thy

Zeta_3_Irrational/

Zeta_3_Irrational.thy

Zeta_Function/

Zeta_Library.thy

tools/

afp_check_roots.scala

afp_dependencies.scala

web/

authors/

aehlig/

bauer/

brinkop/

dirix/

eberl/

edmonds/

esparza/

essmann/

haslbeck/

haslbeckm/

hoelzl/

hu/

jiangd/

klein/

krauss/

lammich/

lochbihler/

michaelis/

milehins/

naraschewski/

neumann/

nipkow/

paulson/

pusch/

rau/

robillard/

rosskopf/

schimpf/

smaus/

somogyi/

sulejmani/

traytel/

urban/

wimmer/

data/

dependencies/

zfc_in_hol/

entries/

Amortized_Complexity.html

Approximation_Algorithms.html

ArrowImpossibilityGS.html

Auto2_HOL.html

Automated_Stateful_Protocol_Verification.html

Boolean_Expression_Checkers.html

CAVA_LTL_Modelchecker.html

CZH_Elementary_Categories.html

CZH_Foundations.html

CZH_Universal_Constructions.html

Category3.html

Closest_Pair_Points.html

Compiling-Exceptions-Correctly.html

Complex_Bounded_Operators.html

Conditional_Simplification.html

Conditional_Transfer_Rule.html

Density_Compiler.html

Dynamic_Tables.html

FOL_Axiomatic.html

Flyspeck-Tame.html

FunWithFunctions.html

FunWithTilings.html

Functional-Automata.html

Gale_Shapley.html

Gauss-Jordan-Elim-Fun.html

LinearQuantifierElim.html

List-Index.html

List_Update.html

Lucas_Theorem.html

MSO_Regex_Equivalence.html

Markov_Models.html

Marriage.html

Metalogic_ProofChecker.html

Prim_Dijkstra_Simple.html

Priority_Queue_Braun.html

Priority_Search_Trees.html

Propositional_Proof_Systems.html

Regex_Equivalence.html

Regular-Sets.html

Root_Balanced_Tree.html

Roth_Arithmetic_Progressions.html

Skew_Heap.html

Smith_Normal_Form.html

Splay_Tree.html

Szemeredi_Regularity.html

Treaps.html

Trie.html

Types_To_Sets_Extension.html

VYDRA_MDL.html

Weight_Balanced_Trees.html

statistics/

theories/

auto2_hol/

automated_stateful_protocol_verification/

category3/

complex_bounded_operators/

czh_elementary_categories/

czh_universal_constructions/

fol_axiomatic/

isabelle_c/

lp_duality/

native_word/

posix-lexing/

smith_normal_form/

vydra_mdl/

word_lib/

rAFP29c7b0c57365

etc/version

metadata/authors.toml

metadata/entries/CZH_Elementary_Categories.toml

metadata/entries/CZH_Foundations.toml

metadata/entries/CZH_Universal_Constructions.toml

metadata/entries/Conditional_Simplification.toml

metadata/entries/Conditional_Transfer_Rule.toml

metadata/entries/Intro_Dest_Elim.toml

metadata/entries/Lucas_Theorem.toml

metadata/entries/Monad_Memo_DP.toml

metadata/entries/Posix-Lexing.toml

metadata/entries/Regular-Sets.toml

metadata/entries/Roth_Arithmetic_Progressions.toml

metadata/entries/Szemeredi_Regularity.toml

metadata/entries/Types_To_Sets_Extension.toml

metadata/entries/Universal_Turing_Machine.toml

metadata/entries/VYDRA_MDL.toml

metadata/entries/WOOT_Strong_Eventual_Consistency.toml

thys/AI_Planning_Languages_Semantics/SASP_Checker.thy

thys/AI_Planning_Languages_Semantics/code/SASP_Checker_Exported.sml

thys/Actuarial_Mathematics/Preliminaries.thy

thys/Affine_Arithmetic/Affine_Approximation.thy

thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy

thys/Affine_Arithmetic/Counterclockwise_2D_Strict.thy

thys/Affine_Arithmetic/Executable_Euclidean_Space.thy

thys/Affine_Arithmetic/Floatarith_Expression.thy

thys/Affine_Arithmetic/Intersection.thy

thys/Affine_Arithmetic/Polygon.thy

thys/Affine_Arithmetic/Straight_Line_Program.thy

thys/Akra_Bazzi/Master_Theorem.thy

thys/Algebraic_Numbers/Real_Roots.thy

thys/Amicable_Numbers/Amicable_Numbers.thy

thys/Auto2_HOL/Auto2_Setup.thy

thys/Auto2_HOL/HOL/Auto2_HOL.thy

thys/Auto2_HOL/HOL/Auto2_HOL_Extra_Setup.thy

thys/Auto2_HOL/HOL/Auto2_HOL_Setup.thy

thys/Auto2_HOL/HOL/Lists_Thms.thy

thys/Auto2_HOL/HOL/Logic_Thms.thy

thys/Auto2_HOL/HOL/Primes_Ex.thy

thys/Auto2_HOL/HOL/Set_Thms.thy

thys/Auto2_HOL/HOL/ac_steps.ML

thys/Auto2_HOL/HOL/acdata.ML

thys/Auto2_HOL/HOL/acdata_test.ML

thys/Auto2_HOL/HOL/arith.ML

thys/Auto2_HOL/HOL/auto2_hol.ML

thys/Auto2_HOL/HOL/auto2_hol_extra_setup.ML

thys/Auto2_HOL/HOL/auto2_hol_util_base.ML

thys/Auto2_HOL/HOL/extra_hol.ML

thys/Auto2_HOL/HOL/induct_outer.ML

thys/Auto2_HOL/HOL/list_ac.ML

thys/Auto2_HOL/HOL/logic_steps_test.ML

thys/Auto2_HOL/HOL/matcher_test.ML

thys/Auto2_HOL/HOL/nat_sub.ML

thys/Auto2_HOL/HOL/nat_sub_test.ML

thys/Auto2_HOL/HOL/normalize_test.ML

thys/Auto2_HOL/HOL/order.ML

thys/Auto2_HOL/HOL/order_test.ML

thys/Auto2_HOL/HOL/rewrite_test.ML

thys/Auto2_HOL/HOL/unfolding.ML

thys/Auto2_HOL/HOL/util_arith.ML

thys/Auto2_HOL/HOL/util_test.ML

thys/Auto2_HOL/ROOT

thys/Auto2_HOL/auto2.ML

thys/Auto2_HOL/auto2_data.ML

thys/Auto2_HOL/auto2_outer.ML

thys/Auto2_HOL/auto2_setup.ML

thys/Auto2_HOL/items.ML

thys/Auto2_HOL/logic_steps.ML

thys/Auto2_HOL/matcher.ML

thys/Auto2_HOL/normalize.ML

thys/Auto2_HOL/proofsteps.ML

thys/Auto2_HOL/property.ML

thys/Auto2_HOL/propertydata.ML

thys/Auto2_HOL/rewrite.ML

thys/Auto2_HOL/status.ML

thys/Auto2_HOL/util_logic.ML

thys/Auto2_HOL/wfdata.ML

thys/Auto2_HOL/wfterm.ML

thys/Auto2_Imperative_HOL/Imperative/SepAuto.thy

thys/Auto2_Imperative_HOL/Imperative/assn_matcher.ML

thys/Auto2_Imperative_HOL/Imperative/list_matcher_test.ML

thys/Auto2_Imperative_HOL/Imperative/sep_steps.ML

thys/Auto2_Imperative_HOL/Imperative/sep_util.ML

thys/Automated_Stateful_Protocol_Verification/Eisbach_Protocol_Verification.thy

thys/Automated_Stateful_Protocol_Verification/Examples.thy

thys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/KeyserverEx.thy

thys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/introduction.thy

thys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/manual.thy

thys/Automated_Stateful_Protocol_Verification/PSPSP.thy

thys/Automated_Stateful_Protocol_Verification/ROOT

thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy

thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy

thys/Automated_Stateful_Protocol_Verification/Term_Abstraction.thy

thys/Automated_Stateful_Protocol_Verification/Term_Implication.thy

thys/Automated_Stateful_Protocol_Verification/Term_Variants.thy

thys/Automated_Stateful_Protocol_Verification/Transactions.thy

thys/Automated_Stateful_Protocol_Verification/document/jedit-keyserver.png

thys/Automated_Stateful_Protocol_Verification/document/jedit-select-session.png

thys/Automated_Stateful_Protocol_Verification/document/lh-listings.sty

thys/Automated_Stateful_Protocol_Verification/document/root.bib

thys/Automated_Stateful_Protocol_Verification/document/root.tex

thys/Automated_Stateful_Protocol_Verification/examples/Keyserver.thy

thys/Automated_Stateful_Protocol_Verification/examples/Keyserver2.thy

thys/Automated_Stateful_Protocol_Verification/examples/Keyserver_Composition.thy

thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model03.thy

thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model07.thy

thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model09.thy

thys/Automated_Stateful_Protocol_Verification/trac/Makefile

thys/Automated_Stateful_Protocol_Verification/trac/bin/ml-lex-isa

thys/Automated_Stateful_Protocol_Verification/trac/bin/ml-yacc-isa

thys/Automated_Stateful_Protocol_Verification/trac/ml_yacc_lib.thy

thys/Automated_Stateful_Protocol_Verification/trac/trac.thy

thys/Automated_Stateful_Protocol_Verification/trac/trac_fp_parser.thy

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.grm

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.grm.sml

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.lex

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.lex.sml

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm.sig

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm.sml

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.lex

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.lex.sml

thys/Automated_Stateful_Protocol_Verification/trac/trac_protocol_parser.thy

thys/Automated_Stateful_Protocol_Verification/trac/trac_term.thy

thys/BD_Security_Compositional/Composing_Security.thy

thys/BD_Security_Compositional/Composing_Security_Network.thy

thys/Banach_Steinhaus/Banach_Steinhaus_Missing.thy

thys/Banach_Steinhaus/document/root.tex

thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy

thys/Bicategory/Bicategory.thy

thys/Bicategory/BicategoryOfSpans.thy

thys/Bicategory/Coherence.thy

thys/Bicategory/EquivalenceOfBicategories.thy

thys/Bicategory/Prebicategory.thy

thys/Bicategory/Pseudofunctor.thy

thys/Bicategory/SpanBicategory.thy

thys/Bicategory/Subbicategory.thy

thys/Blue_Eyes/Blue_Eyes.thy

thys/Bounded_Deducibility_Security/Filtermap.thy

thys/Buffons_Needle/Buffons_Needle.thy

thys/Buildings/Algebra.thy

thys/Buildings/Coxeter.thy

thys/Buildings/Prelim.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_DG_CAT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_DG_FUNCT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_CAT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_CSimplicial.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Category.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Comma.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Conclusions.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Cone.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Discrete.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_FUNCT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Functor.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_GRPH.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Hom.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Introduction.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_NTCF.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Order.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Ordinal.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_PCategory.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Par.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Parallel.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Rel.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_SS.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_SemiCAT.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_Small_Category.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Cone.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Functor.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_NTCF.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Structure_Example.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Subcategory.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Yoneda.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_SMC_CAT.thy

thys/CZH_Elementary_Categories/czh_ecategories/CZH_SMC_FUNCT.thy

thys/CZH_Foundations/ROOT

thys/CZH_Foundations/czh_digraphs/CZH_DG_DGHM.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Digraph.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_GRPH.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Introduction.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_PDigraph.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Par.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Rel.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Set.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Simple.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_DGHM.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_Digraph.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_TDGHM.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_Subdigraph.thy

thys/CZH_Foundations/czh_digraphs/CZH_DG_TDGHM.thy

thys/CZH_Foundations/czh_introduction/CZH_Introduction.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_GRPH.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_NTSMCF.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_PSemicategory.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Par.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Rel.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_SemiCAT.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semicategory.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semifunctor.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Set.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Simple.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_NTSMCF.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_Semicategory.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_Semifunctor.thy

thys/CZH_Foundations/czh_semicategories/CZH_SMC_Subsemicategory.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_BRelations.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_FBRelations.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_FSequences.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_IF.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Introduction.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_NOP.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Nat.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_Sets.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_VNHS.thy

thys/CZH_Foundations/czh_sets/CZH_Sets_ZQR.thy

thys/CZH_Foundations/czh_sets/ex/CZH_EX_Algebra.thy

thys/CZH_Foundations/document/root.bib

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Adjoints.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Comma.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Complete.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Conclusions.thy

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_Limit_Equalizer.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit_IT.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit_Product.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit_Pullback.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan_Example.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Pointed.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Representable.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Set.thy

thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Universal.thy

thys/CZH_Universal_Constructions/document/root.bib

thys/CakeML/Tools/cakeml_compiler.ML

thys/Catalan_Numbers/Catalan_Auxiliary_Integral.thy

thys/Catalan_Numbers/Catalan_Numbers.thy

thys/Category3/Adjunction.thy

thys/Category3/EquivalenceOfCategories.thy

thys/Category3/HFSetCat.thy

thys/Category3/Limit.thy

thys/Category3/ROOT

thys/Category3/SetCat.thy

thys/Category3/SetCategory.thy

thys/Category3/Subcategory.thy

thys/Category3/Yoneda.thy

thys/Category3/ZFC_SetCat.thy

thys/Clique_and_Monotone_Circuits/Assumptions_and_Approximations.thy

thys/Clique_and_Monotone_Circuits/Clique_Large_Monotone_Circuits.thy

thys/Collections/Examples/Autoref/Simple_DFS.thy

thys/Collections/GenCF/Impl/Impl_Bit_Set.thy

thys/Collections/Lib/Code_Target_ICF.thy

thys/Completeness/PermutationLemmas.thy

thys/Completeness/Sequents.thy

thys/Complex_Bounded_Operators/Cblinfun_Code.thy

thys/Complex_Bounded_Operators/Cblinfun_Code_Examples.thy

thys/Complex_Bounded_Operators/Complex_Bounded_Linear_Function.thy

thys/Complex_Bounded_Operators/Complex_L2.thy

thys/Complex_Bounded_Operators/Complex_Vector_Spaces.thy

thys/Complex_Bounded_Operators/One_Dimensional_Spaces.thy

thys/Complex_Bounded_Operators/extra/Extra_General.thy

thys/Complex_Bounded_Operators/extra/Extra_Lattice.thy

thys/Complx/OG_Soundness.thy

thys/Complx/ex/Examples.thy

thys/Conditional_Simplification/CS_Cond_Simp.ML

thys/Conditional_Simplification/CS_Reference.thy

thys/Conditional_Simplification/CS_UM.ML

thys/Conditional_Simplification/IHOL_CS.thy

thys/Core_DOM/standard/Core_DOM_Heap_WF.thy

thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy

thys/Differential_Dynamic_Logic/document/root.bib

thys/Dirichlet_L/Dirichlet_L_Functions.thy

thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy

thys/DiscretePricing/Disc_Cond_Expect.thy

thys/DiscretePricing/Fair_Price.thy

thys/Dominance_CHK/Cfg.thy

thys/Dominance_CHK/Dom_Kildall_Property.thy

thys/DynamicArchitectures/Configuration_Traces.thy

thys/Dynamic_Tables/Tables_nat.thy

thys/Epistemic_Logic/Epistemic_Logic.thy

thys/Ergodic_Theory/Kingman.thy

thys/Error_Function/Error_Function.thy

thys/Error_Function/Error_Function_Asymptotics.thy

thys/Euler_MacLaurin/Euler_MacLaurin.thy

thys/Extended_Finite_State_Machines/EFSM_LTL.thy

thys/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy

thys/FOL_Axiomatic/FOL_Axiomatic.thy

thys/FOL_Axiomatic/FOL_Axiomatic_Variant.thy

thys/FOL_Axiomatic/ROOT

thys/FO_Theory_Rewriting/ROOT

thys/FO_Theory_Rewriting/Util/Multihole_Context.thy

thys/Factor_Algebraic_Polynomial/MPoly_Divide.thy

thys/Finite_Fields/Card_Irreducible_Polynomials_Aux.thy

thys/Flow_Networks/Residual_Graph.thy

thys/Foundation_of_geometry/Congruence.thy

thys/Foundation_of_geometry/Incidence.thy

thys/Foundation_of_geometry/Order.thy

thys/Foundation_of_geometry/document/root.tex

thys/Fourier/Fourier.thy

thys/Frequency_Moments/Frequency_Moment_0.thy

thys/Frequency_Moments/Frequency_Moment_2.thy

thys/Frequency_Moments/Frequency_Moment_k.thy

thys/Frequency_Moments/Frequency_Moments_Preliminary_Results.thy

thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy

thys/Gale_Shapley/Gale_Shapley1.thy

thys/Gale_Shapley/Gale_Shapley2.thy

thys/Game_Based_Crypto/CryptHOL_Tutorial.thy

thys/Girth_Chromatic/Ugraphs.thy

thys/Goedel_HFSet_Semanticless/Sigma.thy

thys/Graph_Theory/Digraph_Isomorphism.thy

thys/Graph_Theory/Kuratowski.thy

thys/Green/Derivs.thy

thys/Green/Integrals.thy

thys/Green/Paths.thy

thys/Groebner_Macaulay/Cone_Decomposition.thy

thys/Groebner_Macaulay/Dube_Bound.thy

thys/Groebner_Macaulay/Dube_Prelims.thy

thys/Grothendieck_Schemes/Comm_Ring.thy

thys/Grothendieck_Schemes/Scheme.thy

thys/Hidden_Markov_Models/Hidden_Markov_Model.thy

thys/Hoare_Time/Big_StepT_Partial.thy

thys/IEEE_Floating_Point/IEEE.thy

thys/IP_Addresses/WordInterval.thy

thys/Incompleteness/Coding.thy

thys/Incompleteness/Predicates.thy

thys/Incompleteness/Sigma.thy

thys/Incompleteness/SyntaxN.thy

thys/Inductive_Inference/LIM_BC.thy

thys/Inductive_Inference/Partial_Recursive.thy

thys/Inductive_Inference/Universal.thy

thys/Interpolation_Polynomials_HOL_Algebra/Bounded_Degree_Polynomials.thy

thys/Interpolation_Polynomials_HOL_Algebra/Interpolation_Polynomial_Cardinalities.thy

thys/Interpolation_Polynomials_HOL_Algebra/Lagrange_Interpolation.thy

thys/Interval_Arithmetic_Word32/Finite_String.thy

thys/Interval_Arithmetic_Word32/Interpreter.thy

thys/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy

thys/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy

thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy

thys/Irrationals_From_THEBOOK/document/root.tex

thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy

thys/Isabelle_C/C11-FrontEnd/C_Main.thy

thys/Isabelle_C/C11-FrontEnd/appendices/C_Appendices.thy

thys/Isabelle_C/C11-FrontEnd/document/root.tex

thys/Isabelle_C/C11-FrontEnd/examples/C0.thy

thys/Isabelle_C/C11-FrontEnd/examples/C1.thy

thys/Isabelle_C/C11-FrontEnd/examples/C2.thy

thys/Isabelle_C/C11-FrontEnd/examples/C3.thy

thys/Isabelle_C/C11-FrontEnd/examples/C4.thy

thys/Isabelle_C/C11-FrontEnd/examples/C_paper.thy

thys/Isabelle_C/C11-FrontEnd/generated/c_grammar_fun.grm.sig

thys/Isabelle_C/C11-FrontEnd/main/C_Main.thy

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

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

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

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

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

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

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

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

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

thys/Isabelle_C/README.thy

thys/Isabelle_C/ROOT

thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_target.thy

thys/JinjaThreads/Basic/Auxiliary.thy

thys/JinjaThreads/Common/ExternalCallWF.thy

thys/JinjaThreads/Compiler/Correctness1.thy

thys/JinjaThreads/Compiler/J1JVMBisim.thy

thys/JinjaThreads/Execute/Random_Scheduler.thy

thys/JinjaThreads/Execute/Scheduler.thy

thys/JinjaThreads/Framework/Bisimulation.thy

thys/JinjaThreads/Framework/LTS.thy

thys/JinjaThreads/MM/JMM_Common.thy

thys/JinjaThreads/MM/JMM_DRF.thy

thys/JinjaThreads/MM/JMM_Framework.thy

thys/JinjaThreads/MM/JMM_Spec.thy

thys/JinjaThreads/MM/JMM_Typesafe.thy

thys/Jordan_Normal_Form/Matrix.thy

thys/LP_Duality/LP_Duality.thy

thys/LP_Duality/Move_To_Matrix.thy

thys/Lambert_W/Lambert_W.thy

thys/Laplace_Transform/Existence.thy

thys/Lifting_the_Exponent/LTE.thy

thys/List_Update/BIT.thy

thys/List_Update/List_Factoring.thy

thys/List_Update/OPT2.thy

thys/List_Update/Prob_Theory.thy

thys/List_Update/TS.thy

thys/Lp/Functional_Spaces.thy

thys/MDP-Rewards/MDP_disc.thy

thys/MFMC_Countable/MFMC_Flow_Attainability.thy

thys/MFMC_Countable/MFMC_Unbounded.thy

thys/MFMC_Countable/MFMC_Web.thy

thys/Markov_Models/Continuous_Time_Markov_Chain.thy

thys/Markov_Models/ex/PCTL.thy

thys/Mereology/CEM.thy

thys/Mereology/CM.thy

thys/Mereology/EM.thy

thys/Mereology/GEM.thy

thys/Mereology/GM.thy

thys/Mereology/M.thy

thys/Mereology/MM.thy

thys/Mereology/PM.thy

thys/Mersenne_Primes/Lucas_Lehmer_Code.thy

thys/MonoidalCategory/FreeMonoidalCategory.thy

thys/Nash_Williams/Nash_Williams.thy

thys/Native_Word/Bits_Integer.thy

thys/Native_Word/Code_Int_Integer_Conversion.thy

thys/Native_Word/Code_Symbolic_Bits_Int.thy

thys/Native_Word/Code_Symbolic_Int_Bit.thy

thys/Native_Word/Code_Target_Bits_Int.thy

thys/Native_Word/Code_Target_Int_Bit.thy

thys/Native_Word/Code_Target_Integer_Bit.thy

thys/Native_Word/Code_Target_Word_Base.thy

thys/Native_Word/Native_Word_Test_Emu.thy

thys/Native_Word/Uint.thy

thys/Native_Word/Uint16.thy

thys/Native_Word/Uint32.thy

thys/Native_Word/Uint64.thy

thys/Native_Word/Uint8.thy

thys/Native_Word/Uint_Userguide.thy

thys/Native_Word/Word_Type_Copies.thy

thys/Nested_Multisets_Ordinals/Multiset_More.thy

thys/Optics/Lens_Record.ML

thys/Ordered_Resolution_Prover/Abstract_Substitution.thy

thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy

thys/Ordinal_Partitions/Partitions.thy

thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy

thys/Ordinary_Differential_Equations/IVP/Cones.thy

thys/Ordinary_Differential_Equations/IVP/Flow.thy

thys/Ordinary_Differential_Equations/IVP/Flow_Congs.thy

thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy

thys/Ordinary_Differential_Equations/IVP/Poincare_Map.thy

thys/Ordinary_Differential_Equations/IVP/Upper_Lower_Solution.thy

thys/Ordinary_Differential_Equations/Library/Gronwall.thy

thys/Ordinary_Differential_Equations/Library/Linear_ODE.thy

thys/Ordinary_Differential_Equations/Library/Vector_Derivative_On.thy

thys/Ordinary_Differential_Equations/Numerics/Concrete_Reachability_Analysis.thy

thys/Ordinary_Differential_Equations/Numerics/Concrete_Reachability_Analysis_C1.thy

thys/Ordinary_Differential_Equations/Numerics/Concrete_Rigorous_Numerics.thy

thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy

thys/Ordinary_Differential_Equations/Numerics/Init_ODE_Solver.thy

thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy

thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis_C1.thy

thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy

thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy

thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy

thys/Ordinary_Differential_Equations/Refinement/Autoref_Misc.thy

thys/Ordinary_Differential_Equations/Refinement/Refine_Default.thy

thys/Ordinary_Differential_Equations/Refinement/Refine_Interval.thy

thys/Ordinary_Differential_Equations/Refinement/Refine_Parallel.thy

thys/Ordinary_Differential_Equations/Refinement/Refine_Vector_List.thy

thys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy

thys/PAC_Checker/PAC_More_Poly.thy

thys/Planarity_Certificates/Planarity/Graph_Genus.thy

thys/Poincare_Bendixson/Analysis_Misc.thy

thys/Poincare_Bendixson/ODE_Misc.thy

thys/Poincare_Bendixson/Poincare_Bendixson.thy

thys/Polynomials/MPoly_Type.thy

thys/Posix-Lexing/Lexer.thy

thys/Posix-Lexing/LexicalVals.thy

thys/Posix-Lexing/Positions.thy

thys/Posix-Lexing/README

thys/Posix-Lexing/ROOT

thys/Posix-Lexing/document/root.tex

thys/Prefix_Free_Code_Combinators/Examples.thy

thys/Prefix_Free_Code_Combinators/Prefix_Free_Code_Combinators.thy

thys/Prime_Distribution_Elementary/Moebius_Mu_Sum.thy

thys/Prime_Distribution_Elementary/Partial_Zeta_Bounds.thy

thys/Prime_Number_Theorem/Mertens_Theorems.thy

thys/Prime_Number_Theorem/Newman_Ingham_Tauberian.thy

thys/Prime_Number_Theorem/Prime_Counting_Functions.thy

thys/Prime_Number_Theorem/Prime_Number_Theorem.thy

thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy

thys/Proof_Strategy_Language/Subtool.ML

thys/Public_Announcement_Logic/PAL.thy

thys/Public_Announcement_Logic/document/root.tex

thys/QHLProver/Complex_Matrix.thy

thys/Quasi_Borel_Spaces/Pair_QuasiBorel_Measure.thy

thys/Quasi_Borel_Spaces/Probability_Space_QuasiBorel.thy

thys/ROOTS

thys/Random_BSTs/Random_BSTs.thy

thys/Random_Graph_Subgraph_Threshold/Ugraph_Lemmas.thy

thys/Real_Power/Log.thy

thys/Real_Power/RealPower.thy

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

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

thys/Refine_Imperative_HOL/Lib/Named_Theorems_Rev.thy

thys/Registers/Quantum_Extra.thy

thys/Registers/document/root.tex

thys/Regular-Sets/Derivatives.thy

thys/Rep_Fin_Groups/Rep_Fin_Groups.thy

thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy

thys/Roth_Arithmetic_Progressions/document/root.tex

thys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy

thys/Safe_Distance/Safe_Distance.thy

thys/Safe_Distance/Safe_Distance_Reaction.thy

thys/Saturation_Framework/Given_Clause_Architectures.thy

thys/Saturation_Framework_Extensions/Clausal_Calculus.thy

thys/Saturation_Framework_Extensions/Standard_Redundancy_Criterion.thy

thys/Schutz_Spacetime/TemporalOrderOnPath.thy

thys/Security_Protocol_Refinement/Refinement/Message.thy

thys/Signature_Groebner/Prelims.thy

thys/Smith_Normal_Form/Alternative_Proofs.thy

thys/Smith_Normal_Form/ROOT

thys/Smooth_Manifolds/Analysis_More.thy

thys/Smooth_Manifolds/Bump_Function.thy

thys/Smooth_Manifolds/Chart.thy

thys/Smooth_Manifolds/Cotangent_Space.thy

thys/Smooth_Manifolds/Projective_Space.thy

thys/Smooth_Manifolds/Tangent_Space.thy

thys/Sophomores_Dream/Sophomores_Dream.thy

thys/Special_Function_Bounds/ROOT

thys/Stateful_Protocol_Composition_and_Typing/Examples.thy

thys/Stateful_Protocol_Composition_and_Typing/Intruder_Deduction.thy

thys/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy

thys/Stateful_Protocol_Composition_and_Typing/Labeled_Strands.thy

thys/Stateful_Protocol_Composition_and_Typing/Lazy_Intruder.thy

thys/Stateful_Protocol_Composition_and_Typing/Messages.thy

thys/Stateful_Protocol_Composition_and_Typing/Miscellaneous.thy

thys/Stateful_Protocol_Composition_and_Typing/More_Unification.thy

thys/Stateful_Protocol_Composition_and_Typing/Parallel_Compositionality.thy

thys/Stateful_Protocol_Composition_and_Typing/ROOT

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Strands.thy

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Typing.thy

thys/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy

thys/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy

thys/Stateful_Protocol_Composition_and_Typing/Typing_Result.thy

thys/Stateful_Protocol_Composition_and_Typing/document/root.tex

thys/Stateful_Protocol_Composition_and_Typing/examples/Example_Keyserver.thy

thys/Stateful_Protocol_Composition_and_Typing/examples/Example_TLS.thy

thys/Stirling_Formula/Gamma_Asymptotics.thy

thys/Stirling_Formula/Stirling_Formula.thy

thys/Store_Buffer_Reduction/SyntaxTweaks.thy

thys/Sturm_Sequences/Sturm_Method.thy

thys/Sunflowers/Erdos_Rado_Sunflower.thy

thys/Sunflowers/document/root.bib

thys/Sunflowers/document/root.tex

thys/Szemeredi_Regularity/Szemeredi.thy

thys/Szemeredi_Regularity/document/root.tex

thys/Taylor_Models/Taylor_Models.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Topology/SML_Product_Topology.thy

thys/Types_To_Sets_Extension/Examples/SML_Relativization/Topology/SML_Topological_Space.thy

thys/UpDown_Scheme/Triangular_Function.thy

thys/VYDRA_MDL/Interval.thy

thys/VYDRA_MDL/Metric_Point_Structure.thy

thys/VYDRA_MDL/Monitor_Code.thy

thys/VYDRA_MDL/NFA.thy

thys/VYDRA_MDL/ROOT

thys/VYDRA_MDL/Timestamp.thy

thys/VYDRA_MDL/Timestamp_Lex.thy

thys/VYDRA_MDL/Timestamp_Lex_Total.thy

thys/VYDRA_MDL/Timestamp_Prod.thy

thys/VYDRA_MDL/Trace.thy

thys/VYDRA_MDL/document/root.bib

thys/VYDRA_MDL/document/root.tex

thys/Van_Emde_Boas_Trees/ROOT

thys/VerifyThis2019/Challenge3.thy

thys/Virtual_Substitution/Debruijn.thy

thys/Virtual_Substitution/EliminateVariable.thy

thys/Virtual_Substitution/ExecutiblePolyProps.thy

thys/Virtual_Substitution/OptimizationProofs.thy

thys/WOOT_Strong_Eventual_Consistency/Consistency.thy

thys/WOOT_Strong_Eventual_Consistency/CreateConsistent.thy

thys/WOOT_Strong_Eventual_Consistency/DistributedExecution.thy

thys/WOOT_Strong_Eventual_Consistency/IntegrateAlgorithm.thy

thys/WOOT_Strong_Eventual_Consistency/IntegrateInsertCommute.thy

thys/WOOT_Strong_Eventual_Consistency/Psi.thy

thys/WOOT_Strong_Eventual_Consistency/SortKeys.thy

thys/WebAssembly/Wasm_Printing/Wasm_Interpreter_Printing_Pure.thy

thys/Weight_Balanced_Trees/Weight_Balanced_Trees_log.thy

thys/Weighted_Path_Order/WPO.thy

thys/Wetzels_Problem/Wetzels_Problem.thy

thys/Word_Lib/Ancient_Numeral.thy

thys/Word_Lib/Bit_Comprehension.thy

thys/Word_Lib/Bits_Int.thy

thys/Word_Lib/Generic_set_bit.thy

thys/Word_Lib/Guide.thy

thys/Word_Lib/Least_significant_bit.thy

thys/Word_Lib/Many_More.thy

thys/Word_Lib/More_Word.thy

thys/Word_Lib/More_Word_Operations.thy

thys/Word_Lib/ROOT

thys/Word_Lib/Reversed_Bit_Lists.thy

thys/Word_Lib/Word_Lemmas.thy

thys/X86_Semantics/X86_Parse.ML

thys/Youngs_Inequality/document/root.tex

thys/ZFC_in_HOL/General_Cardinals.thy

thys/ZFC_in_HOL/Kirby.thy

thys/ZFC_in_HOL/Ordinal_Exp.thy

thys/ZFC_in_HOL/ROOT

thys/ZFC_in_HOL/ZFC_Cardinals.thy

thys/ZFC_in_HOL/ZFC_Typeclasses.thy

thys/ZFC_in_HOL/ZFC_in_HOL.thy

thys/Zeta_3_Irrational/Zeta_3_Irrational.thy

thys/Zeta_Function/Zeta_Library.thy

tools/afp_check_roots.scala

tools/afp_dependencies.scala

web/authors/aehlig/index.html

web/authors/bauer/index.html

web/authors/brinkop/index.html

web/authors/dirix/index.html

web/authors/eberl/index.html

web/authors/edmonds/index.html

web/authors/esparza/index.html

web/authors/essmann/index.html

web/authors/haslbeck/index.html

web/authors/haslbeckm/index.html

web/authors/hoelzl/index.html

web/authors/hu/index.html

web/authors/jiangd/index.html

web/authors/klein/index.html

web/authors/krauss/index.html

web/authors/lammich/index.html

web/authors/lochbihler/index.html

web/authors/michaelis/index.html

web/authors/milehins/index.html

web/authors/naraschewski/index.html

web/authors/neumann/index.html

web/authors/nipkow/index.html

web/authors/paulson/index.html

web/authors/pusch/index.html

web/authors/rau/index.html

web/authors/robillard/index.html

web/authors/rosskopf/index.html

web/authors/schimpf/index.html

web/authors/smaus/index.html

web/authors/somogyi/index.html

web/authors/sulejmani/index.html

web/authors/traytel/index.html

web/authors/urban/index.html

web/authors/wimmer/index.html

web/data/keywords.json

web/dependencies/zfc_in_hol/index.html

web/dependencies/zfc_in_hol/index.xml

web/entries/AVL-Trees.html

web/entries/Abs_Int_ITP2012.html

web/entries/Abstract-Hoare-Logics.html

web/entries/Amortized_Complexity.html

web/entries/Approximation_Algorithms.html

web/entries/ArrowImpossibilityGS.html

web/entries/Auto2_HOL.html

web/entries/Automated_Stateful_Protocol_Verification.html

web/entries/Boolean_Expression_Checkers.html

web/entries/CAVA_LTL_Modelchecker.html

web/entries/CZH_Elementary_Categories.html

web/entries/CZH_Foundations.html

web/entries/CZH_Universal_Constructions.html

web/entries/Category3.html

web/entries/Closest_Pair_Points.html

web/entries/Compiling-Exceptions-Correctly.html

web/entries/Complex_Bounded_Operators.html

web/entries/Conditional_Simplification.html

web/entries/Conditional_Transfer_Rule.html

web/entries/Density_Compiler.html

web/entries/Dynamic_Tables.html

web/entries/FOL_Axiomatic.html

web/entries/Flyspeck-Tame.html

web/entries/FunWithFunctions.html

web/entries/FunWithTilings.html

web/entries/Functional-Automata.html

web/entries/Gale_Shapley.html

web/entries/Gauss-Jordan-Elim-Fun.html

web/entries/Hoare_Time.html

web/entries/HotelKeyCards.html

web/entries/Intro_Dest_Elim.html

web/entries/Isabelle_C.html

web/entries/Jinja.html

web/entries/LP_Duality.html

web/entries/LinearQuantifierElim.html

web/entries/List-Index.html

web/entries/List_Update.html

web/entries/Lucas_Theorem.html

web/entries/MSO_Regex_Equivalence.html

web/entries/Markov_Models.html

web/entries/Marriage.html

web/entries/Metalogic_ProofChecker.html

web/entries/MiniML.html

web/entries/Monad_Memo_DP.html

web/entries/Native_Word.html

web/entries/NormByEval.html

web/entries/Optimal_BST.html

web/entries/Pairing_Heap.html

web/entries/Posix-Lexing.html

web/entries/Prim_Dijkstra_Simple.html

web/entries/Priority_Queue_Braun.html

web/entries/Priority_Search_Trees.html

web/entries/Propositional_Proof_Systems.html

web/entries/Regex_Equivalence.html

web/entries/Regular-Sets.html

web/entries/Root_Balanced_Tree.html

web/entries/Roth_Arithmetic_Progressions.html

web/entries/Skew_Heap.html

web/entries/Smith_Normal_Form.html

web/entries/Splay_Tree.html

web/entries/Szemeredi_Regularity.html

web/entries/Treaps.html

web/entries/Trie.html

web/entries/Types_To_Sets_Extension.html

web/entries/VYDRA_MDL.html

web/entries/Weight_Balanced_Trees.html

web/entries/Word_Lib.html

web/entries/ZFC_in_HOL.html

web/index.html

web/index.json

web/index.xml

web/statistics/index.html

web/theories/auto2_hol/index.html

web/theories/automated_stateful_protocol_verification/index.html

web/theories/category3/index.html

web/theories/complex_bounded_operators/index.html

web/theories/czh_elementary_categories/index.html

web/theories/czh_universal_constructions/index.html

web/theories/fol_axiomatic/index.html

web/theories/isabelle_c/index.html

web/theories/lp_duality/index.html

web/theories/native_word/index.html

web/theories/posix-lexing/index.html

web/theories/smith_normal_form/index.html

web/theories/vydra_mdl/index.html