Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

merged
more generous timeout (25min CPU time);
non-executable files;

Changeset 11594:db241c4c36c8 by wenzelm: merged
Changeset 11593:51acef257c90 by wenzelm: more generous timeout (25min CPU time);
The file was modified	`thys/JinjaDCI/ROOT`
Changeset 11592:02a4bc4b6ee8 by wenzelm: non-executable files;
The file was modified	`thys/Approximation_Algorithms/Approx_BP_Hoare.thy`
The file was modified	`thys/Approximation_Algorithms/Approx_MIS_Hoare.thy`
The file was modified	`thys/Arith_Prog_Rel_Primes/Arith_Prog_Rel_Primes.thy`
The file was modified	`thys/Arith_Prog_Rel_Primes/ROOT`
The file was modified	`thys/Arith_Prog_Rel_Primes/document/root.bib`
The file was modified	`thys/Arith_Prog_Rel_Primes/document/root.tex`
The file was modified	`thys/Complete_Non_Orders/Binary_Relations.thy`
The file was modified	`thys/Complete_Non_Orders/Complete_Relations.thy`
The file was modified	`thys/Complex_Geometry/document/root.tex`
The file was modified	`thys/Extended_Finite_State_Machine_Inference/document/root.bib`
The file was modified	`thys/Extended_Finite_State_Machine_Inference/document/root.tex`
The file was modified	`thys/Extended_Finite_State_Machines/EFSM_LTL.thy`
The file was modified	`thys/Groebner_Macaulay/Binomial_Int.thy`
The file was modified	`thys/Groebner_Macaulay/Cone_Decomposition.thy`
The file was modified	`thys/Groebner_Macaulay/Degree_Bound_Utils.thy`
The file was modified	`thys/Groebner_Macaulay/Degree_Section.thy`
The file was modified	`thys/Groebner_Macaulay/Dube_Bound.thy`
The file was modified	`thys/Groebner_Macaulay/Dube_Prelims.thy`
The file was modified	`thys/Groebner_Macaulay/Groebner_Macaulay.thy`
The file was modified	`thys/Groebner_Macaulay/Groebner_Macaulay_Examples.thy`
The file was modified	`thys/Groebner_Macaulay/Hilbert_Function.thy`
The file was modified	`thys/Groebner_Macaulay/Monomial_Module.thy`
The file was modified	`thys/Groebner_Macaulay/Poly_Fun.thy`
The file was modified	`thys/Groebner_Macaulay/ROOT`
The file was modified	`thys/Groebner_Macaulay/document/root.bib`
The file was modified	`thys/Groebner_Macaulay/document/root.tex`
The file was modified	`thys/Isabelle_Marries_Dirac/Basics.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Binary_Nat.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Complex_Vectors.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Deutsch.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Deutsch_Jozsa.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Entanglement.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Measurement.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/More_Tensor.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/No_Cloning.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Quantum.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Quantum_Prisoners_Dilemma.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/Quantum_Teleportation.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/README.md`
The file was modified	`thys/Isabelle_Marries_Dirac/ROOT`
The file was modified	`thys/Isabelle_Marries_Dirac/Tensor.thy`
The file was modified	`thys/Isabelle_Marries_Dirac/document/root.bib`
The file was modified	`thys/Isabelle_Marries_Dirac/document/root.tex`
The file was modified	`thys/JinjaDCI/Common/Auxiliary.thy`
The file was modified	`thys/JinjaDCI/Common/Conform.thy`
The file was modified	`thys/JinjaDCI/Common/Decl.thy`
The file was modified	`thys/JinjaDCI/Common/Exceptions.thy`
The file was modified	`thys/JinjaDCI/Common/Objects.thy`
The file was modified	`thys/JinjaDCI/Common/SystemClasses.thy`
The file was modified	`thys/JinjaDCI/Common/Type.thy`
The file was modified	`thys/JinjaDCI/Common/TypeRel.thy`
The file was modified	`thys/JinjaDCI/Common/Value.thy`
The file was modified	`thys/JinjaDCI/Common/WellForm.thy`
The file was modified	`thys/JinjaDCI/Compiler/Compiler.thy`
The file was modified	`thys/JinjaDCI/Compiler/Compiler1.thy`
The file was modified	`thys/JinjaDCI/Compiler/Compiler2.thy`
The file was modified	`thys/JinjaDCI/Compiler/Correctness1.thy`
The file was modified	`thys/JinjaDCI/Compiler/Correctness2.thy`
The file was modified	`thys/JinjaDCI/Compiler/Hidden.thy`
The file was modified	`thys/JinjaDCI/Compiler/J1.thy`
The file was modified	`thys/JinjaDCI/Compiler/J1WellForm.thy`
The file was modified	`thys/JinjaDCI/Compiler/PCompiler.thy`
The file was modified	`thys/JinjaDCI/Compiler/TypeComp.thy`
The file was modified	`thys/JinjaDCI/J/Annotate.thy`
The file was modified	`thys/JinjaDCI/J/BigStep.thy`
The file was modified	`thys/JinjaDCI/J/DefAss.thy`
The file was modified	`thys/JinjaDCI/J/EConform.thy`
The file was modified	`thys/JinjaDCI/J/Equivalence.thy`
The file was modified	`thys/JinjaDCI/J/Examples.thy`
The file was modified	`thys/JinjaDCI/J/Expr.thy`
The file was modified	`thys/JinjaDCI/J/JWellForm.thy`
The file was modified	`thys/JinjaDCI/J/Progress.thy`
The file was modified	`thys/JinjaDCI/J/SmallStep.thy`
The file was modified	`thys/JinjaDCI/J/State.thy`
The file was modified	`thys/JinjaDCI/J/TypeSafe.thy`
The file was modified	`thys/JinjaDCI/J/WWellForm.thy`
The file was modified	`thys/JinjaDCI/J/WellType.thy`
The file was modified	`thys/JinjaDCI/J/WellTypeRT.thy`
The file was modified	`thys/JinjaDCI/J/execute_Bigstep.thy`
The file was modified	`thys/JinjaDCI/J/execute_WellType.thy`
The file was modified	`thys/JinjaDCI/JVM/JVMDefensive.thy`
The file was modified	`thys/JinjaDCI/JVM/JVMExceptions.thy`
The file was modified	`thys/JinjaDCI/JVM/JVMExec.thy`
The file was modified	`thys/JinjaDCI/JVM/JVMExecInstr.thy`
The file was modified	`thys/JinjaDCI/JVM/JVMInstructions.thy`
The file was modified	`thys/JinjaDCI/JVM/JVMState.thy`
The file was modified	`thys/JinjaDCI/JinjaDCI.thy`
The file was modified	`thys/JinjaDCI/document/root.bib`
The file was modified	`thys/Laplace_Transform/Existence.thy`
The file was modified	`thys/Laplace_Transform/Laplace_Transform.thy`
The file was modified	`thys/Laplace_Transform/Laplace_Transform_Library.thy`
The file was modified	`thys/Laplace_Transform/Lerch_Lemma.thy`
The file was modified	`thys/Laplace_Transform/Piecewise_Continuous.thy`
The file was modified	`thys/Laplace_Transform/ROOT`
The file was modified	`thys/Laplace_Transform/Uniqueness.thy`
The file was modified	`thys/Laplace_Transform/document/root.bib`
The file was modified	`thys/Laplace_Transform/document/root.tex`
The file was modified	`thys/Nullstellensatz/Algebraically_Closed_Fields.thy`
The file was modified	`thys/Nullstellensatz/Lex_Order_PP.thy`
The file was modified	`thys/Nullstellensatz/Nullstellensatz.thy`
The file was modified	`thys/Nullstellensatz/Nullstellensatz_Field.thy`
The file was modified	`thys/Nullstellensatz/ROOT`
The file was modified	`thys/Nullstellensatz/Univariate_PM.thy`
The file was modified	`thys/Nullstellensatz/document/root.bib`
The file was modified	`thys/Nullstellensatz/document/root.tex`
The file was modified	`thys/Physical_Quantities/Groups_mult.thy`
The file was modified	`thys/Physical_Quantities/ISQ.thy`
The file was modified	`thys/Physical_Quantities/ISQ_Algebra.thy`
The file was modified	`thys/Physical_Quantities/ISQ_Dimensions.thy`
The file was modified	`thys/Physical_Quantities/ISQ_Proof.thy`
The file was modified	`thys/Physical_Quantities/ISQ_Quantities.thy`
The file was modified	`thys/Physical_Quantities/ROOT`
The file was modified	`thys/Physical_Quantities/SI.thy`
The file was modified	`thys/Physical_Quantities/SI_Accepted.thy`
The file was modified	`thys/Physical_Quantities/SI_Astronomical.thy`
The file was modified	`thys/Physical_Quantities/SI_Constants.thy`
The file was modified	`thys/Physical_Quantities/SI_Derived.thy`
The file was modified	`thys/Physical_Quantities/SI_Imperial.thy`
The file was modified	`thys/Physical_Quantities/SI_Prefix.thy`
The file was modified	`thys/Physical_Quantities/SI_Units.thy`
The file was modified	`thys/Physical_Quantities/document/adb-long.bib`
The file was modified	`thys/Physical_Quantities/document/root.bib`
The file was modified	`thys/Physical_Quantities/document/root.tex`
The file was modified	`thys/Poincare_Bendixson/Affine_Arithmetic_Misc.thy`
The file was modified	`thys/Poincare_Bendixson/Analysis_Misc.thy`
The file was modified	`thys/Poincare_Bendixson/Examples.thy`
The file was modified	`thys/Poincare_Bendixson/Invariance.thy`
The file was modified	`thys/Poincare_Bendixson/Limit_Set.thy`
The file was modified	`thys/Poincare_Bendixson/ODE_Misc.thy`
The file was modified	`thys/Poincare_Bendixson/Periodic_Orbit.thy`
The file was modified	`thys/Poincare_Bendixson/Poincare_Bendixson.thy`
The file was modified	`thys/Poincare_Bendixson/ROOT`
The file was modified	`thys/Poincare_Bendixson/document/root.tex`
The file was modified	`thys/Poincare_Disc/document/root.tex`
The file was modified	`thys/Universal_Turing_Machine/Rec_Def.thy`