diff --git a/thys/Approximation_Algorithms/Approx_BP_Hoare.thy b/thys/Approximation_Algorithms/Approx_BP_Hoare.thy old mode 100755 new mode 100644 diff --git a/thys/Approximation_Algorithms/Approx_MIS_Hoare.thy b/thys/Approximation_Algorithms/Approx_MIS_Hoare.thy old mode 100755 new mode 100644 diff --git a/thys/Arith_Prog_Rel_Primes/Arith_Prog_Rel_Primes.thy b/thys/Arith_Prog_Rel_Primes/Arith_Prog_Rel_Primes.thy old mode 100755 new mode 100644 diff --git a/thys/Arith_Prog_Rel_Primes/ROOT b/thys/Arith_Prog_Rel_Primes/ROOT old mode 100755 new mode 100644 diff --git a/thys/Arith_Prog_Rel_Primes/document/root.bib b/thys/Arith_Prog_Rel_Primes/document/root.bib old mode 100755 new mode 100644 diff --git a/thys/Arith_Prog_Rel_Primes/document/root.tex b/thys/Arith_Prog_Rel_Primes/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Complete_Non_Orders/Binary_Relations.thy b/thys/Complete_Non_Orders/Binary_Relations.thy old mode 100755 new mode 100644 diff --git a/thys/Complete_Non_Orders/Complete_Relations.thy b/thys/Complete_Non_Orders/Complete_Relations.thy old mode 100755 new mode 100644 diff --git a/thys/Complex_Geometry/document/root.tex b/thys/Complex_Geometry/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Extended_Finite_State_Machine_Inference/document/root.bib b/thys/Extended_Finite_State_Machine_Inference/document/root.bib old mode 100755 new mode 100644 diff --git a/thys/Extended_Finite_State_Machine_Inference/document/root.tex b/thys/Extended_Finite_State_Machine_Inference/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Extended_Finite_State_Machines/EFSM_LTL.thy b/thys/Extended_Finite_State_Machines/EFSM_LTL.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Binomial_Int.thy b/thys/Groebner_Macaulay/Binomial_Int.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Cone_Decomposition.thy b/thys/Groebner_Macaulay/Cone_Decomposition.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Degree_Bound_Utils.thy b/thys/Groebner_Macaulay/Degree_Bound_Utils.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Degree_Section.thy b/thys/Groebner_Macaulay/Degree_Section.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Dube_Bound.thy b/thys/Groebner_Macaulay/Dube_Bound.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Dube_Prelims.thy b/thys/Groebner_Macaulay/Dube_Prelims.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Groebner_Macaulay.thy b/thys/Groebner_Macaulay/Groebner_Macaulay.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy b/thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Hilbert_Function.thy b/thys/Groebner_Macaulay/Hilbert_Function.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Monomial_Module.thy b/thys/Groebner_Macaulay/Monomial_Module.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/Poly_Fun.thy b/thys/Groebner_Macaulay/Poly_Fun.thy old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/ROOT b/thys/Groebner_Macaulay/ROOT old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/document/root.bib b/thys/Groebner_Macaulay/document/root.bib old mode 100755 new mode 100644 diff --git a/thys/Groebner_Macaulay/document/root.tex b/thys/Groebner_Macaulay/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Basics.thy b/thys/Isabelle_Marries_Dirac/Basics.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Binary_Nat.thy b/thys/Isabelle_Marries_Dirac/Binary_Nat.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Complex_Vectors.thy b/thys/Isabelle_Marries_Dirac/Complex_Vectors.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Deutsch.thy b/thys/Isabelle_Marries_Dirac/Deutsch.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Deutsch_Jozsa.thy b/thys/Isabelle_Marries_Dirac/Deutsch_Jozsa.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Entanglement.thy b/thys/Isabelle_Marries_Dirac/Entanglement.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Measurement.thy b/thys/Isabelle_Marries_Dirac/Measurement.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/More_Tensor.thy b/thys/Isabelle_Marries_Dirac/More_Tensor.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/No_Cloning.thy b/thys/Isabelle_Marries_Dirac/No_Cloning.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Quantum.thy b/thys/Isabelle_Marries_Dirac/Quantum.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Quantum_Prisoners_Dilemma.thy b/thys/Isabelle_Marries_Dirac/Quantum_Prisoners_Dilemma.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Quantum_Teleportation.thy b/thys/Isabelle_Marries_Dirac/Quantum_Teleportation.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/README.md b/thys/Isabelle_Marries_Dirac/README.md old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/ROOT b/thys/Isabelle_Marries_Dirac/ROOT old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/Tensor.thy b/thys/Isabelle_Marries_Dirac/Tensor.thy old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/document/root.bib b/thys/Isabelle_Marries_Dirac/document/root.bib old mode 100755 new mode 100644 diff --git a/thys/Isabelle_Marries_Dirac/document/root.tex b/thys/Isabelle_Marries_Dirac/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/Auxiliary.thy b/thys/JinjaDCI/Common/Auxiliary.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/Conform.thy b/thys/JinjaDCI/Common/Conform.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/Decl.thy b/thys/JinjaDCI/Common/Decl.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/Exceptions.thy b/thys/JinjaDCI/Common/Exceptions.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/Objects.thy b/thys/JinjaDCI/Common/Objects.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/SystemClasses.thy b/thys/JinjaDCI/Common/SystemClasses.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/Type.thy b/thys/JinjaDCI/Common/Type.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/TypeRel.thy b/thys/JinjaDCI/Common/TypeRel.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/Value.thy b/thys/JinjaDCI/Common/Value.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Common/WellForm.thy b/thys/JinjaDCI/Common/WellForm.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/Compiler.thy b/thys/JinjaDCI/Compiler/Compiler.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/Compiler1.thy b/thys/JinjaDCI/Compiler/Compiler1.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/Compiler2.thy b/thys/JinjaDCI/Compiler/Compiler2.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/Correctness1.thy b/thys/JinjaDCI/Compiler/Correctness1.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/Correctness2.thy b/thys/JinjaDCI/Compiler/Correctness2.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/Hidden.thy b/thys/JinjaDCI/Compiler/Hidden.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/J1.thy b/thys/JinjaDCI/Compiler/J1.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/J1WellForm.thy b/thys/JinjaDCI/Compiler/J1WellForm.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/PCompiler.thy b/thys/JinjaDCI/Compiler/PCompiler.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/Compiler/TypeComp.thy b/thys/JinjaDCI/Compiler/TypeComp.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/Annotate.thy b/thys/JinjaDCI/J/Annotate.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/BigStep.thy b/thys/JinjaDCI/J/BigStep.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/DefAss.thy b/thys/JinjaDCI/J/DefAss.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/EConform.thy b/thys/JinjaDCI/J/EConform.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/Equivalence.thy b/thys/JinjaDCI/J/Equivalence.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/Examples.thy b/thys/JinjaDCI/J/Examples.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/Expr.thy b/thys/JinjaDCI/J/Expr.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/JWellForm.thy b/thys/JinjaDCI/J/JWellForm.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/Progress.thy b/thys/JinjaDCI/J/Progress.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/SmallStep.thy b/thys/JinjaDCI/J/SmallStep.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/State.thy b/thys/JinjaDCI/J/State.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/TypeSafe.thy b/thys/JinjaDCI/J/TypeSafe.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/WWellForm.thy b/thys/JinjaDCI/J/WWellForm.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/WellType.thy b/thys/JinjaDCI/J/WellType.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/WellTypeRT.thy b/thys/JinjaDCI/J/WellTypeRT.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/execute_Bigstep.thy b/thys/JinjaDCI/J/execute_Bigstep.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/J/execute_WellType.thy b/thys/JinjaDCI/J/execute_WellType.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/JVM/JVMDefensive.thy b/thys/JinjaDCI/JVM/JVMDefensive.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/JVM/JVMExceptions.thy b/thys/JinjaDCI/JVM/JVMExceptions.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/JVM/JVMExec.thy b/thys/JinjaDCI/JVM/JVMExec.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/JVM/JVMExecInstr.thy b/thys/JinjaDCI/JVM/JVMExecInstr.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/JVM/JVMInstructions.thy b/thys/JinjaDCI/JVM/JVMInstructions.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/JVM/JVMState.thy b/thys/JinjaDCI/JVM/JVMState.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/JinjaDCI.thy b/thys/JinjaDCI/JinjaDCI.thy old mode 100755 new mode 100644 diff --git a/thys/JinjaDCI/ROOT b/thys/JinjaDCI/ROOT --- a/thys/JinjaDCI/ROOT +++ b/thys/JinjaDCI/ROOT @@ -1,18 +1,18 @@ chapter AFP session JinjaDCI (AFP) = "HOL-Library" + - options [timeout = 1200, document = pdf] + options [timeout = 2400, document = pdf] sessions "List-Index" "Jinja" directories "BV" "Common" "Compiler" "J" "JVM" theories JinjaDCI document_files "root.bib" "root.tex" diff --git a/thys/JinjaDCI/document/root.bib b/thys/JinjaDCI/document/root.bib old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/Existence.thy b/thys/Laplace_Transform/Existence.thy old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/Laplace_Transform.thy b/thys/Laplace_Transform/Laplace_Transform.thy old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/Laplace_Transform_Library.thy b/thys/Laplace_Transform/Laplace_Transform_Library.thy old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/Lerch_Lemma.thy b/thys/Laplace_Transform/Lerch_Lemma.thy old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/Piecewise_Continuous.thy b/thys/Laplace_Transform/Piecewise_Continuous.thy old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/ROOT b/thys/Laplace_Transform/ROOT old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/Uniqueness.thy b/thys/Laplace_Transform/Uniqueness.thy old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/document/root.bib b/thys/Laplace_Transform/document/root.bib old mode 100755 new mode 100644 diff --git a/thys/Laplace_Transform/document/root.tex b/thys/Laplace_Transform/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Nullstellensatz/Algebraically_Closed_Fields.thy b/thys/Nullstellensatz/Algebraically_Closed_Fields.thy old mode 100755 new mode 100644 diff --git a/thys/Nullstellensatz/Lex_Order_PP.thy b/thys/Nullstellensatz/Lex_Order_PP.thy old mode 100755 new mode 100644 diff --git a/thys/Nullstellensatz/Nullstellensatz.thy b/thys/Nullstellensatz/Nullstellensatz.thy old mode 100755 new mode 100644 diff --git a/thys/Nullstellensatz/Nullstellensatz_Field.thy b/thys/Nullstellensatz/Nullstellensatz_Field.thy old mode 100755 new mode 100644 diff --git a/thys/Nullstellensatz/ROOT b/thys/Nullstellensatz/ROOT old mode 100755 new mode 100644 diff --git a/thys/Nullstellensatz/Univariate_PM.thy b/thys/Nullstellensatz/Univariate_PM.thy old mode 100755 new mode 100644 diff --git a/thys/Nullstellensatz/document/root.bib b/thys/Nullstellensatz/document/root.bib old mode 100755 new mode 100644 diff --git a/thys/Nullstellensatz/document/root.tex b/thys/Nullstellensatz/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/Groups_mult.thy b/thys/Physical_Quantities/Groups_mult.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/ISQ.thy b/thys/Physical_Quantities/ISQ.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/ISQ_Algebra.thy b/thys/Physical_Quantities/ISQ_Algebra.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/ISQ_Dimensions.thy b/thys/Physical_Quantities/ISQ_Dimensions.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/ISQ_Proof.thy b/thys/Physical_Quantities/ISQ_Proof.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/ISQ_Quantities.thy b/thys/Physical_Quantities/ISQ_Quantities.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/ROOT b/thys/Physical_Quantities/ROOT old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/SI.thy b/thys/Physical_Quantities/SI.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/SI_Accepted.thy b/thys/Physical_Quantities/SI_Accepted.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/SI_Astronomical.thy b/thys/Physical_Quantities/SI_Astronomical.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/SI_Constants.thy b/thys/Physical_Quantities/SI_Constants.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/SI_Derived.thy b/thys/Physical_Quantities/SI_Derived.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/SI_Imperial.thy b/thys/Physical_Quantities/SI_Imperial.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/SI_Prefix.thy b/thys/Physical_Quantities/SI_Prefix.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/SI_Units.thy b/thys/Physical_Quantities/SI_Units.thy old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/document/adb-long.bib b/thys/Physical_Quantities/document/adb-long.bib old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/document/root.bib b/thys/Physical_Quantities/document/root.bib old mode 100755 new mode 100644 diff --git a/thys/Physical_Quantities/document/root.tex b/thys/Physical_Quantities/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy b/thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/Analysis_Misc.thy b/thys/Poincare_Bendixson/Analysis_Misc.thy old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/Examples.thy b/thys/Poincare_Bendixson/Examples.thy old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/Invariance.thy b/thys/Poincare_Bendixson/Invariance.thy old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/Limit_Set.thy b/thys/Poincare_Bendixson/Limit_Set.thy old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/ODE_Misc.thy b/thys/Poincare_Bendixson/ODE_Misc.thy old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/Periodic_Orbit.thy b/thys/Poincare_Bendixson/Periodic_Orbit.thy old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/Poincare_Bendixson.thy b/thys/Poincare_Bendixson/Poincare_Bendixson.thy old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/ROOT b/thys/Poincare_Bendixson/ROOT old mode 100755 new mode 100644 diff --git a/thys/Poincare_Bendixson/document/root.tex b/thys/Poincare_Bendixson/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Poincare_Disc/document/root.tex b/thys/Poincare_Disc/document/root.tex old mode 100755 new mode 100644 diff --git a/thys/Universal_Turing_Machine/Rec_Def.thy b/thys/Universal_Turing_Machine/Rec_Def.thy old mode 100755 new mode 100644