HomeIsabelle/Phabricator
Diffusion afp-devel 02a4bc4b6ee8

non-executable files;
02a4bc4b6ee8
Actions

Description

non-executable files;

Details

Provenance
makariusAuthored on
Parents
rAFPeb0cc2599588: adjustments for Word_Lib updates
Branches
Unknown
Tags
Unknown

Changes (135)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.
PathSize
thys/
Approximation_Algorithms/
Arith_Prog_Rel_Primes/
document/
Complete_Non_Orders/
Complex_Geometry/
document/
Extended_Finite_State_Machine_Inference/
document/
Extended_Finite_State_Machines/
Groebner_Macaulay/
document/
Isabelle_Marries_Dirac/
document/
JinjaDCI/
Common/
Compiler/
J/
JVM/
document/
Laplace_Transform/
document/
Nullstellensatz/
document/
Physical_Quantities/
document/
Poincare_Bendixson/
document/
Poincare_Disc/
document/
Universal_Turing_Machine/

rAFP02a4bc4b6ee8

View Options

thys/Approximation_Algorithms/Approx_BP_Hoare.thy

View Options

thys/Approximation_Algorithms/Approx_MIS_Hoare.thy

View Options

thys/Arith_Prog_Rel_Primes/Arith_Prog_Rel_Primes.thy

View Options

thys/Arith_Prog_Rel_Primes/ROOT

View Options

thys/Arith_Prog_Rel_Primes/document/root.bib

View Options

thys/Arith_Prog_Rel_Primes/document/root.tex

View Options

thys/Complete_Non_Orders/Binary_Relations.thy

View Options

thys/Complete_Non_Orders/Complete_Relations.thy

View Options

thys/Complex_Geometry/document/root.tex

View Options

thys/Extended_Finite_State_Machine_Inference/document/root.bib

View Options

thys/Extended_Finite_State_Machine_Inference/document/root.tex

View Options

thys/Extended_Finite_State_Machines/EFSM_LTL.thy

View Options

thys/Groebner_Macaulay/Binomial_Int.thy

View Options

thys/Groebner_Macaulay/Cone_Decomposition.thy

View Options

thys/Groebner_Macaulay/Degree_Bound_Utils.thy

View Options

thys/Groebner_Macaulay/Degree_Section.thy

View Options

thys/Groebner_Macaulay/Dube_Bound.thy

View Options

thys/Groebner_Macaulay/Dube_Prelims.thy

View Options

thys/Groebner_Macaulay/Groebner_Macaulay.thy

View Options

thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy

View Options

thys/Groebner_Macaulay/Hilbert_Function.thy

View Options

thys/Groebner_Macaulay/Monomial_Module.thy

View Options

thys/Groebner_Macaulay/Poly_Fun.thy

View Options

thys/Groebner_Macaulay/ROOT

View Options

thys/Groebner_Macaulay/document/root.bib

View Options

thys/Groebner_Macaulay/document/root.tex

View Options

thys/Isabelle_Marries_Dirac/Basics.thy

View Options

thys/Isabelle_Marries_Dirac/Binary_Nat.thy

View Options

thys/Isabelle_Marries_Dirac/Complex_Vectors.thy

View Options

thys/Isabelle_Marries_Dirac/Deutsch.thy

View Options

thys/Isabelle_Marries_Dirac/Deutsch_Jozsa.thy

View Options

thys/Isabelle_Marries_Dirac/Entanglement.thy

View Options

thys/Isabelle_Marries_Dirac/Measurement.thy

View Options

thys/Isabelle_Marries_Dirac/More_Tensor.thy

View Options

thys/Isabelle_Marries_Dirac/No_Cloning.thy

View Options

thys/Isabelle_Marries_Dirac/Quantum.thy

View Options

thys/Isabelle_Marries_Dirac/Quantum_Prisoners_Dilemma.thy

View Options

thys/Isabelle_Marries_Dirac/Quantum_Teleportation.thy

View Options

thys/Isabelle_Marries_Dirac/README.md

View Options

thys/Isabelle_Marries_Dirac/ROOT

View Options

thys/Isabelle_Marries_Dirac/Tensor.thy

View Options

thys/Isabelle_Marries_Dirac/document/root.bib

View Options

thys/Isabelle_Marries_Dirac/document/root.tex

View Options

thys/JinjaDCI/Common/Auxiliary.thy

View Options

thys/JinjaDCI/Common/Conform.thy

View Options

thys/JinjaDCI/Common/Decl.thy

View Options

thys/JinjaDCI/Common/Exceptions.thy

View Options

thys/JinjaDCI/Common/Objects.thy

View Options

thys/JinjaDCI/Common/SystemClasses.thy

View Options

thys/JinjaDCI/Common/Type.thy

View Options

thys/JinjaDCI/Common/TypeRel.thy

View Options

thys/JinjaDCI/Common/Value.thy

View Options

thys/JinjaDCI/Common/WellForm.thy

View Options

thys/JinjaDCI/Compiler/Compiler.thy

View Options

thys/JinjaDCI/Compiler/Compiler1.thy

View Options

thys/JinjaDCI/Compiler/Compiler2.thy

View Options

thys/JinjaDCI/Compiler/Correctness1.thy

View Options

thys/JinjaDCI/Compiler/Correctness2.thy

View Options

thys/JinjaDCI/Compiler/Hidden.thy

View Options

thys/JinjaDCI/Compiler/J1.thy

View Options

thys/JinjaDCI/Compiler/J1WellForm.thy

View Options

thys/JinjaDCI/Compiler/PCompiler.thy

View Options

thys/JinjaDCI/Compiler/TypeComp.thy

View Options

thys/JinjaDCI/J/Annotate.thy

View Options

thys/JinjaDCI/J/BigStep.thy

View Options

thys/JinjaDCI/J/DefAss.thy

View Options

thys/JinjaDCI/J/EConform.thy

View Options

thys/JinjaDCI/J/Equivalence.thy

View Options

thys/JinjaDCI/J/Examples.thy

View Options

thys/JinjaDCI/J/Expr.thy

View Options

thys/JinjaDCI/J/JWellForm.thy

View Options

thys/JinjaDCI/J/Progress.thy

View Options

thys/JinjaDCI/J/SmallStep.thy

View Options

thys/JinjaDCI/J/State.thy

View Options

thys/JinjaDCI/J/TypeSafe.thy

View Options

thys/JinjaDCI/J/WWellForm.thy

View Options

thys/JinjaDCI/J/WellType.thy

View Options

thys/JinjaDCI/J/WellTypeRT.thy

View Options

thys/JinjaDCI/J/execute_Bigstep.thy

View Options

thys/JinjaDCI/J/execute_WellType.thy

View Options

thys/JinjaDCI/JVM/JVMDefensive.thy

View Options

thys/JinjaDCI/JVM/JVMExceptions.thy

View Options

thys/JinjaDCI/JVM/JVMExec.thy

View Options

thys/JinjaDCI/JVM/JVMExecInstr.thy

View Options

thys/JinjaDCI/JVM/JVMInstructions.thy

View Options

thys/JinjaDCI/JVM/JVMState.thy

View Options

thys/JinjaDCI/JinjaDCI.thy

View Options

thys/JinjaDCI/document/root.bib

View Options

thys/Laplace_Transform/Existence.thy

View Options

thys/Laplace_Transform/Laplace_Transform.thy

View Options

thys/Laplace_Transform/Laplace_Transform_Library.thy

View Options

thys/Laplace_Transform/Lerch_Lemma.thy

View Options

thys/Laplace_Transform/Piecewise_Continuous.thy

View Options

thys/Laplace_Transform/ROOT

View Options

thys/Laplace_Transform/Uniqueness.thy

View Options

thys/Laplace_Transform/document/root.bib

View Options

thys/Laplace_Transform/document/root.tex

View Options

thys/Nullstellensatz/Algebraically_Closed_Fields.thy

View Options

thys/Nullstellensatz/Lex_Order_PP.thy

View Options

thys/Nullstellensatz/Nullstellensatz.thy

View Options

thys/Nullstellensatz/Nullstellensatz_Field.thy

View Options

thys/Nullstellensatz/ROOT

View Options

thys/Nullstellensatz/Univariate_PM.thy

View Options

thys/Nullstellensatz/document/root.bib

View Options

thys/Nullstellensatz/document/root.tex

View Options

thys/Physical_Quantities/Groups_mult.thy

View Options

thys/Physical_Quantities/ISQ.thy

View Options

thys/Physical_Quantities/ISQ_Algebra.thy

View Options

thys/Physical_Quantities/ISQ_Dimensions.thy

View Options

thys/Physical_Quantities/ISQ_Proof.thy

View Options

thys/Physical_Quantities/ISQ_Quantities.thy

View Options

thys/Physical_Quantities/ROOT

View Options

thys/Physical_Quantities/SI.thy

View Options

thys/Physical_Quantities/SI_Accepted.thy

View Options

thys/Physical_Quantities/SI_Astronomical.thy

View Options

thys/Physical_Quantities/SI_Constants.thy

View Options

thys/Physical_Quantities/SI_Derived.thy

View Options

thys/Physical_Quantities/SI_Imperial.thy

View Options

thys/Physical_Quantities/SI_Prefix.thy

View Options

thys/Physical_Quantities/SI_Units.thy

View Options

thys/Physical_Quantities/document/adb-long.bib

View Options

thys/Physical_Quantities/document/root.bib

View Options

thys/Physical_Quantities/document/root.tex

View Options

thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy

View Options

thys/Poincare_Bendixson/Analysis_Misc.thy

View Options

thys/Poincare_Bendixson/Examples.thy

View Options

thys/Poincare_Bendixson/Invariance.thy

View Options

thys/Poincare_Bendixson/Limit_Set.thy

View Options

thys/Poincare_Bendixson/ODE_Misc.thy

View Options

thys/Poincare_Bendixson/Periodic_Orbit.thy

View Options

thys/Poincare_Bendixson/Poincare_Bendixson.thy

View Options

thys/Poincare_Bendixson/ROOT

View Options

thys/Poincare_Bendixson/document/root.tex

View Options

thys/Poincare_Disc/document/root.tex

View Options

thys/Universal_Turing_Machine/Rec_Def.thy