Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. added documentation for changes to Sledgehammer option "lam_trans"
  3. jenkins: pre/post-hook results
  4. merged
  5. added opaque_combs and renamed hide_lams to opaque_lifting
  6. more robust treatment of empty string;
  7. invoke Scala compiler from Java, without external process; tuned messages;
  8. clarified version: Apple now counts like 11, 12, ...;
  9. Imported lots of material from Stirling_Formula/Gamma_Asymptotics
Changeset 73936:d593d18a7a92 by desharna:
merged
Changeset 73935:269b2f976100 by desharna:
added documentation for changes to Sledgehammer option "lam_trans"
The file was modified CONTRIBUTORS
The file was modified NEWS
The file was modified src/Doc/Sledgehammer/document/root.tex
Changeset 73934:39e0c7fac69e by fabian huch _huch@in.tum.de_:
jenkins: pre/post-hook results
The file was modified src/Pure/Admin/ci_profile.scala
Changeset 73933:fa92bc604c59 by desharna:
merged
Changeset 73932:fd21b4a93043 by desharna:
added opaque_combs and renamed hide_lams to opaque_lifting
The file was modified src/Doc/Sledgehammer/document/root.tex
The file was modified src/HOL/Algebra/Coset.thy
The file was modified src/HOL/Algebra/Free_Abelian_Groups.thy
The file was modified src/HOL/Algebra/Generated_Groups.thy
The file was modified src/HOL/Algebra/Group.thy
The file was modified src/HOL/Algebra/Polynomial_Divisibility.thy
The file was modified src/HOL/Algebra/Product_Groups.thy
The file was modified src/HOL/Algebra/Subrings.thy
The file was modified src/HOL/Analysis/Abstract_Topology.thy
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy
The file was modified src/HOL/Analysis/Arcwise_Connected.thy
The file was modified src/HOL/Analysis/Bochner_Integration.thy
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy
The file was modified src/HOL/Analysis/Cartesian_Space.thy
The file was modified src/HOL/Analysis/Change_Of_Vars.thy
The file was modified src/HOL/Analysis/Complex_Transcendental.thy
The file was modified src/HOL/Analysis/Connected.thy
The file was modified src/HOL/Analysis/Cross3.thy
The file was modified src/HOL/Analysis/Derivative.thy
The file was modified src/HOL/Analysis/Determinants.thy
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
The file was modified src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy
The file was modified src/HOL/Analysis/Function_Metric.thy
The file was modified src/HOL/Analysis/Further_Topology.thy
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
The file was modified src/HOL/Analysis/Homotopy.thy
The file was modified src/HOL/Analysis/Jordan_Curve.thy
The file was modified src/HOL/Analysis/Line_Segment.thy
The file was modified src/HOL/Analysis/Linear_Algebra.thy
The file was modified src/HOL/Analysis/Path_Connected.thy
The file was modified src/HOL/Analysis/Polytope.thy
The file was modified src/HOL/Analysis/Retracts.thy
The file was modified src/HOL/Analysis/Starlike.thy
The file was modified src/HOL/Analysis/Tagged_Division.thy
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy
The file was modified src/HOL/Analysis/Uniform_Limit.thy
The file was modified src/HOL/Auth/Message.thy
The file was modified src/HOL/Binomial.thy
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy
The file was modified src/HOL/Combinatorics/Cycles.thy
The file was modified src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
The file was modified src/HOL/Complex_Analysis/Complex_Singularities.thy
The file was modified src/HOL/Complex_Analysis/Conformal_Mappings.thy
The file was modified src/HOL/Complex_Analysis/Great_Picard.thy
The file was modified src/HOL/Complex_Analysis/Riemann_Mapping.thy
The file was modified src/HOL/Complex_Analysis/Winding_Numbers.thy
The file was modified src/HOL/Computational_Algebra/Polynomial.thy
The file was modified src/HOL/Deriv.thy
The file was modified src/HOL/Homology/Brouwer_Degree.thy
The file was modified src/HOL/Homology/Invariance_of_Domain.thy
The file was modified src/HOL/Homology/Simplices.thy
The file was modified src/HOL/IMP/Abs_Int2.thy
The file was modified src/HOL/IMP/Abs_Int3.thy
The file was modified src/HOL/Library/Dlist.thy
The file was modified src/HOL/Library/Equipollence.thy
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy
The file was modified src/HOL/Library/Extended_Real.thy
The file was modified src/HOL/Library/Float.thy
The file was modified src/HOL/Library/FuncSet.thy
The file was modified src/HOL/Library/Interval.thy
The file was modified src/HOL/Library/Poly_Mapping.thy
The file was modified src/HOL/Library/Word.thy
The file was modified src/HOL/List.thy
The file was modified src/HOL/Nominal/Examples/Class1.thy
The file was modified src/HOL/Nonstandard_Analysis/NSA.thy
The file was modified src/HOL/Probability/Conditional_Expectation.thy
The file was modified src/HOL/Quotient_Examples/Lift_Fun.thy
The file was modified src/HOL/Real.thy
The file was modified src/HOL/Real_Vector_Spaces.thy
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
The file was modified src/HOL/Series.thy
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML
The file was modified src/HOL/Tools/Metis/metis_generate.ML
The file was modified src/HOL/Tools/Metis/metis_tactic.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
The file was modified src/HOL/Transcendental.thy
The file was modified src/HOL/Vector_Spaces.thy
The file was modified src/HOL/ex/Dedekind_Real.thy
Changeset 73931:4a708e150908 by wenzelm:
more robust treatment of empty string;
The file was modified src/Tools/Setup/isabelle/setup/Build_Scala.java
Changeset 73930:17c09d1b3588 by wenzelm:
invoke Scala compiler from Java, without external process;<br>tuned messages;
The file was modified Admin/lib/Tools/build_setup
The file was modified src/Tools/Setup/isabelle/setup/Build_Scala.java
The file was modified src/Tools/Setup/isabelle/setup/Environment.java
Changeset 73929:7d15ebca4bb3 by wenzelm:
clarified version: Apple now counts like 11, 12, ...;
The file was modified src/Pure/Admin/isabelle_cronjob.scala
Changeset 73928:3b76524f5a85 by paulson _lp15@cam.ac.uk_:
Imported lots of material from Stirling_Formula/Gamma_Asymptotics
The file was modified NEWS
The file was modified src/HOL/Analysis/Change_Of_Vars.thy
The file was modified src/HOL/Analysis/Complex_Transcendental.thy
The file was modified src/HOL/Analysis/Derivative.thy
The file was modified src/HOL/Analysis/Gamma_Function.thy
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
The file was modified src/HOL/Complex.thy
The file was modified src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
The file was modified src/HOL/Library/Indicator_Function.thy

Summary

  1. T1 fontenc for new entries
  2. sitegen
  3. update hide_lams -> opaque_lifting
  4. merged from afp2021
  5. website for SpecCheck
  6. new entry SpecCheck
  7. metadata and sitegen for MiniSail
  8. new entry: MiniSail
  9. sitegen for Public Announcement Logic
  10. new entry "Public Announcement Logic" (and sorted ROOTS + removed duplicate entries in ROOTS)
  11. fixed a messy reference
  12. Van_der_Waerden website
  13. new entry Van_der_Waerden
  14. New entry IMP_Compiler
  15. Removal of unintended files
  16. Hidden.thy to Isar
  17. merged
  18. renamed hide_lams opaque_lifting
  19. merged
  20. jenkins: pre/post-hook results
  21. changed to opaque_lifiting as suggested by Isabelle/Jenkins
  22. changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins
  23. Added missing Public_Announcement_Logic to ROOTS file
  24. More Support on Clean Syntax, Basic Lens Support, New Examples.
  25. finishing arg -> Arg and moving some material out of Stirling_Formula/Gamma_Asymptotics
Changeset 11923:a8a03d5e5117 by andreas lochbihler _mail@andreas-lochbihler.de_:
T1 fontenc for new entries
The file was modified thys/IMP_Compiler/document/root.tex
The file was modified thys/MiniSail/document/root.tex
The file was modified thys/Public_Announcement_Logic/document/root.tex
The file was modified thys/Van_der_Waerden/document/root.tex
Changeset 11922:2992e460f579 by andreas lochbihler _mail@andreas-lochbihler.de_:
sitegen
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11921:1c2e8c2011c9 by andreas lochbihler _mail@andreas-lochbihler.de_:
update hide_lams -&gt; opaque_lifting
The file was modified thys/MiniSail/BTVSubst.thy
The file was modified thys/MiniSail/Nominal-Utils.thy
The file was modified thys/MiniSail/Safety.thy
The file was modified thys/MiniSail/Syntax.thy
The file was modified thys/MiniSail/WellformedL.thy
Changeset 11920:a60ccd2e9cc6 by andreas lochbihler _mail@andreas-lochbihler.de_:
merged from afp2021
Changeset 11919:4e8ba94d4183 by andreas lochbihler _mail@andreas-lochbihler.de_:
website for SpecCheck
The file was addedweb/entries/SpecCheck.html
The file was modified metadata/metadata
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11918:44d6d533286d by andreas lochbihler _mail@andreas-lochbihler.de_:
new entry SpecCheck
The file was addedthys/SpecCheck/README.md
The file was addedthys/SpecCheck/ROOT
The file was addedthys/SpecCheck/SpecCheck.thy
The file was addedthys/SpecCheck/SpecCheck_Base.thy
The file was addedthys/SpecCheck/configuration.ML
The file was addedthys/SpecCheck/document/root.tex
The file was addedthys/SpecCheck/dynamic/SpecCheck_Dynamic.thy
The file was addedthys/SpecCheck/dynamic/dynamic_construct.ML
The file was addedthys/SpecCheck/dynamic/speccheck_dynamic.ML
The file was addedthys/SpecCheck/examples/SpecCheck_Examples.thy
The file was addedthys/SpecCheck/generators/SpecCheck_Generators.thy
The file was addedthys/SpecCheck/generators/gen.ML
The file was addedthys/SpecCheck/generators/gen_base.ML
The file was addedthys/SpecCheck/generators/gen_function.ML
The file was addedthys/SpecCheck/generators/gen_int.ML
The file was addedthys/SpecCheck/generators/gen_real.ML
The file was addedthys/SpecCheck/generators/gen_term.ML
The file was addedthys/SpecCheck/generators/gen_text.ML
The file was addedthys/SpecCheck/generators/gen_types.ML
The file was addedthys/SpecCheck/lecker.ML
The file was addedthys/SpecCheck/output_styles/SpecCheck_Output_Style.thy
The file was addedthys/SpecCheck/output_styles/output_style.ML
The file was addedthys/SpecCheck/output_styles/output_style_custom.ML
The file was addedthys/SpecCheck/output_styles/output_style_perl.ML
The file was addedthys/SpecCheck/output_styles/output_style_types.ML
The file was addedthys/SpecCheck/property.ML
The file was addedthys/SpecCheck/random.ML
The file was addedthys/SpecCheck/show/SpecCheck_Show.thy
The file was addedthys/SpecCheck/show/show.ML
The file was addedthys/SpecCheck/show/show_base.ML
The file was addedthys/SpecCheck/show/show_types.ML
The file was addedthys/SpecCheck/shrink/SpecCheck_Shrink.thy
The file was addedthys/SpecCheck/shrink/shrink.ML
The file was addedthys/SpecCheck/shrink/shrink_base.ML
The file was addedthys/SpecCheck/shrink/shrink_types.ML
The file was addedthys/SpecCheck/speccheck.ML
The file was addedthys/SpecCheck/speccheck_base.ML
The file was addedthys/SpecCheck/util.ML
The file was modified thys/ROOTS
Changeset 11917:b44bedc236cb by rene thiemann _rene.thiemann@uibk.ac.at_:
metadata and sitegen for MiniSail
The file was addedweb/entries/MiniSail.html
The file was modified metadata/metadata
The file was modified web/entries/Native_Word.html
The file was modified web/entries/Nominal2.html
The file was modified web/entries/Show.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11916:336dfa0f0b93 by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: MiniSail
The file was addedthys/MiniSail/BTVSubst.thy
The file was addedthys/MiniSail/BTVSubstTypingL.thy
The file was addedthys/MiniSail/ContextSubtypingL.thy
The file was addedthys/MiniSail/Examples.thy
The file was addedthys/MiniSail/IVSubst.thy
The file was addedthys/MiniSail/IVSubstTypingL.thy
The file was addedthys/MiniSail/MiniSail.thy
The file was addedthys/MiniSail/Nominal-Utils.thy
The file was addedthys/MiniSail/Operational.thy
The file was addedthys/MiniSail/RCLogic.thy
The file was addedthys/MiniSail/RCLogicL.thy
The file was addedthys/MiniSail/ROOT
The file was addedthys/MiniSail/Safety.thy
The file was addedthys/MiniSail/SubstMethods.thy
The file was addedthys/MiniSail/Syntax.thy
The file was addedthys/MiniSail/SyntaxL.thy
The file was addedthys/MiniSail/Typing.thy
The file was addedthys/MiniSail/TypingL.thy
The file was addedthys/MiniSail/Wellformed.thy
The file was addedthys/MiniSail/WellformedL.thy
The file was addedthys/MiniSail/document/root.bib
The file was addedthys/MiniSail/document/root.tex
The file was modified thys/ROOTS
Changeset 11915:81eccfc5a0e3 by rene thiemann _rene.thiemann@uibk.ac.at_:
sitegen for Public Announcement Logic
The file was addedweb/entries/Public_Announcement_Logic.html
The file was modified metadata/metadata
The file was modified web/entries/Epistemic_Logic.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11914:d764bf06a728 by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry &quot;Public Announcement Logic&quot;<br>(and sorted ROOTS + removed duplicate entries in ROOTS)
The file was addedthys/Public_Announcement_Logic/PAL.thy
The file was addedthys/Public_Announcement_Logic/ROOT
The file was addedthys/Public_Announcement_Logic/document/root.bib
The file was addedthys/Public_Announcement_Logic/document/root.tex
The file was modified thys/ROOTS
Changeset 11913:2241611aef17 by paulson _lp15@cam.ac.uk_:
fixed a messy reference
The file was modified thys/Van_der_Waerden/document/root.bib
The file was modified thys/Van_der_Waerden/document/root.tex
Changeset 11912:1f48f33779db by paulson _lp15@cam.ac.uk_:
Van_der_Waerden website
The file was addedweb/entries/Van_der_Waerden.html
The file was modified metadata/metadata
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11911:a3c7e21a602f by paulson _lp15@cam.ac.uk_:
new entry Van_der_Waerden
The file was addedthys/Van_der_Waerden/Digits.thy
The file was addedthys/Van_der_Waerden/ROOT
The file was addedthys/Van_der_Waerden/Van_der_Waerden.thy
The file was addedthys/Van_der_Waerden/document/root.bib
The file was addedthys/Van_der_Waerden/document/root.tex
The file was modified thys/ROOTS
Changeset 11910:6424fbf12644 by nipkow:
New entry IMP_Compiler
The file was addedthys/IMP_Compiler/Compiler.thy
The file was addedthys/IMP_Compiler/Compiler2.thy
The file was addedthys/IMP_Compiler/ROOT
The file was addedthys/IMP_Compiler/document/root.bib
The file was addedthys/IMP_Compiler/document/root.tex
The file was addedweb/entries/IMP_Compiler.html
The file was modified metadata/metadata
The file was modified thys/ROOTS
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11909:fe45d0404b6b by susannah mansky _susannahej@gmail.com_:
Removal of unintended files
The file was removedthys/JinjaDCI/BV/BVExample.thy
The file was removedthys/JinjaDCI/J/Examples.thy
The file was removedthys/JinjaDCI/J/execute_Bigstep.thy
The file was removedthys/JinjaDCI/J/execute_WellType.thy
Changeset 11908:6de5937fcbcb by susannah mansky _susannahej@gmail.com_:
Hidden.thy to Isar
The file was modified thys/Jinja/Compiler/Hidden.thy
The file was modified thys/JinjaDCI/Compiler/Hidden.thy
Changeset 11907:a3060bc70b44 by desharna:
merged
Changeset 11906:975b2b1d8a19 by desharna:
renamed hide_lams opaque_lifting
The file was modified thys/AI_Planning_Languages_Semantics/PDDL_STRIPS_Semantics.thy
The file was modified thys/AI_Planning_Languages_Semantics/SASP_Checker.thy
The file was modified thys/AODV/Fresher.thy
The file was modified thys/AODV/variants/a_norreqid/A_Fresher.thy
The file was modified thys/AODV/variants/b_fwdrreps/B_Fresher.thy
The file was modified thys/AODV/variants/c_gtobcast/C_Fresher.thy
The file was modified thys/AODV/variants/d_fwdrreqs/D_Fresher.thy
The file was modified thys/AODV/variants/e_all_abcd/E_Fresher.thy
The file was modified thys/AWN/Pnet.thy
The file was modified thys/Adaptive_State_Counting/ASC/ASC_Sufficiency.thy
The file was modified thys/Adaptive_State_Counting/ASC/ASC_Suite.thy
The file was modified thys/Adaptive_State_Counting/ATC/ATC.thy
The file was modified thys/Adaptive_State_Counting/FSM/FSM.thy
The file was modified thys/Affine_Arithmetic/Affine_Form.thy
The file was modified thys/Affine_Arithmetic/Floatarith_Expression.thy
The file was modified thys/Affine_Arithmetic/Intersection.thy
The file was modified thys/Aggregation_Algebras/Matrix_Aggregation_Algebras.thy
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy
The file was modified thys/Amicable_Numbers/Amicable_Numbers.thy
The file was modified thys/Approximation_Algorithms/Approx_BP_Hoare.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Term_Implication.thy
The file was modified thys/Automatic_Refinement/Lib/Misc.thy
The file was modified thys/BTree/BTree_ImpSplit.thy
The file was modified thys/BTree/BTree_Set.thy
The file was modified thys/Banach_Steinhaus/Banach_Steinhaus.thy
The file was modified thys/Banach_Steinhaus/Banach_Steinhaus_Missing.thy
The file was modified thys/BenOr_Kozen_Reif/BKR_Decision.thy
The file was modified thys/BenOr_Kozen_Reif/Matrix_Equation_Construction.thy
The file was modified thys/BenOr_Kozen_Reif/Renegar_Decision.thy
The file was modified thys/BenOr_Kozen_Reif/Renegar_Proofs.thy
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy
The file was modified thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy
The file was modified thys/Berlekamp_Zassenhaus/Distinct_Degree_Factorization.thy
The file was modified thys/Bicategory/SpanBicategory.thy
The file was modified thys/Binding_Syntax_Theory/Iteration.thy
The file was modified thys/Binding_Syntax_Theory/Semantic_Domains.thy
The file was modified thys/Binding_Syntax_Theory/Transition_QuasiTerms_Terms.thy
The file was modified thys/BirdKMP/HOLCF_ROOT.thy
The file was modified thys/BirdKMP/KMP.thy
The file was modified thys/Budan_Fourier/BF_Misc.thy
The file was modified thys/Buildings/Algebra.thy
The file was modified thys/CAVA_Automata/Simulation.thy
The file was modified thys/CISC-Kernel/trace/Rushby-with-Control/SK.thy
The file was modified thys/CakeML_Codegen/Backend/CakeML_Correctness.thy
The file was modified thys/Call_Arity/ArityAnalysisAbinds.thy
The file was modified thys/Call_Arity/CoCallImplSafe.thy
The file was modified thys/Chandy_Lamport/Snapshot.thy
The file was modified thys/Chandy_Lamport/Swap.thy
The file was modified thys/Chandy_Lamport/Util.thy
The file was modified thys/Coinductive/Examples/LMirror.thy
The file was modified thys/Collections/GenCF/Gen/Gen_Map.thy
The file was modified thys/Complex_Geometry/Linear_Systems.thy
The file was modified thys/Complex_Geometry/More_Complex.thy
The file was modified thys/Complex_Geometry/More_Transcendental.thy
The file was modified thys/ComponentDependencies/DataDependenciesCaseStudy.thy
The file was modified thys/ConcurrentGC/Global_Invariants_Lemmas.thy
The file was modified thys/ConcurrentGC/Local_Invariants_Lemmas.thy
The file was modified thys/ConcurrentGC/Noninterference.thy
The file was modified thys/ConcurrentGC/StrongTricolour.thy
The file was modified thys/ConcurrentIMP/Infinite_Sequences.thy
The file was modified thys/ConcurrentIMP/LTL.thy
The file was modified thys/Consensus_Refined/Observing/BenOr_Proofs.thy
The file was modified thys/Constructive_Cryptography_CM/Constructions/One_Time_Pad.thy
The file was modified thys/Containers/Examples/Containers_TwoSat_Ex.thy
The file was modified thys/Core_DOM/common/Core_DOM_Functions.thy
The file was modified thys/Core_DOM/common/monads/CharacterDataMonad.thy
The file was modified thys/Core_DOM/common/monads/DocumentMonad.thy
The file was modified thys/Core_DOM/common/monads/ElementMonad.thy
The file was modified thys/Core_DOM/standard/Core_DOM_Heap_WF.thy
The file was modified thys/Core_SC_DOM/common/Core_DOM_Functions.thy
The file was modified thys/Core_SC_DOM/common/monads/CharacterDataMonad.thy
The file was modified thys/Core_SC_DOM/common/monads/DocumentMonad.thy
The file was modified thys/Core_SC_DOM/common/monads/ElementMonad.thy
The file was modified thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy
The file was modified thys/Count_Complex_Roots/Count_Complex_Roots.thy
The file was modified thys/Count_Complex_Roots/More_Polynomials.thy
The file was modified thys/CryptHOL/GPV_Expectation.thy
The file was modified thys/DOM_Components/Core_DOM_Components.thy
The file was modified thys/Decreasing-Diagrams/Decreasing_Diagrams.thy
The file was modified thys/Dependent_SIFUM_Refinement/Examples/Eg1Eg2RefinementSimple.thy
The file was modified thys/Dependent_SIFUM_Refinement/Examples/EgHighBranchRevC.thy
The file was modified thys/Dependent_SIFUM_Type_Systems/Compositionality.thy
The file was modified thys/Dependent_SIFUM_Type_Systems/LocallySoundModeUse.thy
The file was modified thys/Dependent_SIFUM_Type_Systems/TypeSystem.thy
The file was modified thys/Derangements/Derangements.thy
The file was modified thys/Differential_Game_Logic/Coincidence.thy
The file was modified thys/Differential_Game_Logic/USubst.thy
The file was modified thys/DiscretePricing/CRR_Model.thy
The file was modified thys/DiscretePricing/Disc_Cond_Expect.thy
The file was modified thys/DiscretePricing/Fair_Price.thy
The file was modified thys/DiscretePricing/Infinite_Coin_Toss_Space.thy
The file was modified thys/Echelon_Form/Echelon_Form.thy
The file was modified thys/Echelon_Form/Echelon_Form_IArrays.thy
The file was modified thys/Epistemic_Logic/Epistemic_Logic.thy
The file was modified thys/Ergodic_Theory/Invariants.thy
The file was modified thys/Ergodic_Theory/Normalizing_Sequences.thy
The file was modified thys/Ergodic_Theory/Transfer_Operator.thy
The file was modified thys/Extended_Finite_State_Machine_Inference/Subsumption.thy
The file was modified thys/Extended_Finite_State_Machines/Trilean.thy
The file was modified thys/FLP/Execution.thy
The file was modified thys/FLP/FLPTheorem.thy
The file was modified thys/Featherweight_OCL/UML_PropertyProfiles.thy
The file was modified thys/Featherweight_OCL/UML_State.thy
The file was modified thys/Featherweight_OCL/collection_types/UML_Bag.thy
The file was modified thys/Featherweight_OCL/collection_types/UML_Set.thy
The file was modified thys/Formal_SSA/FormalSSA_Misc.thy
The file was modified thys/Formula_Derivatives/WS1S_Formula.thy
The file was modified thys/FunWithFunctions/FunWithFunctions.thy
The file was modified thys/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy
The file was modified thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy
The file was modified thys/Gabow_SCC/Gabow_Skeleton.thy
The file was modified thys/Gauss_Jordan/Determinants2.thy
The file was modified thys/Gauss_Jordan/Elementary_Operations.thy
The file was modified thys/Gauss_Jordan/Inverse.thy
The file was modified thys/Gauss_Jordan/Linear_Maps.thy
The file was modified thys/Gauss_Jordan/System_Of_Equations.thy
The file was modified thys/Generic_Join/Generic_Join_Correctness.thy
The file was modified thys/Graph_Theory/Digraph_Component.thy
The file was modified thys/Green/CircExample.thy
The file was modified thys/Green/DiamExample.thy
The file was modified thys/Green/Paths.thy
The file was modified thys/Groebner_Bases/Algorithm_Schema.thy
The file was modified thys/Gromov_Hyperbolicity/Bonk_Schramm_Extension.thy
The file was modified thys/Gromov_Hyperbolicity/Busemann_Function.thy
The file was modified thys/Gromov_Hyperbolicity/Eexp_Eln.thy
The file was modified thys/Gromov_Hyperbolicity/Gromov_Boundary.thy
The file was modified thys/Gromov_Hyperbolicity/Gromov_Hyperbolicity.thy
The file was modified thys/Gromov_Hyperbolicity/Isometries_Classification.thy
The file was modified thys/Gromov_Hyperbolicity/Library_Complements.thy
The file was modified thys/Gromov_Hyperbolicity/Morse_Gromov_Theorem.thy
The file was modified thys/Grothendieck_Schemes/Comm_Ring.thy
The file was modified thys/HOL-CSP/CSP.thy
The file was modified thys/HOL-CSP/Mndet.thy
The file was modified thys/HOL-CSP/Sync.thy
The file was modified thys/Hoare_Time/Big_StepT_Partial.thy
The file was modified thys/Hoare_Time/QuantK_Hoare.thy
The file was modified thys/Hoare_Time/Quant_Hoare.thy
The file was modified thys/Hybrid_Logic/Hybrid_Logic.thy
The file was modified thys/Hybrid_Multi_Lane_Spatial_Logic/HMLSL.thy
The file was modified thys/Hybrid_Multi_Lane_Spatial_Logic/Length.thy
The file was modified thys/Hybrid_Multi_Lane_Spatial_Logic/NatInt.thy
The file was modified thys/Hybrid_Multi_Lane_Spatial_Logic/RealInt.thy
The file was modified thys/Hybrid_Multi_Lane_Spatial_Logic/Restriction.thy
The file was modified thys/Hybrid_Multi_Lane_Spatial_Logic/Sensors.thy
The file was modified thys/Hybrid_Multi_Lane_Spatial_Logic/Views.thy
The file was modified thys/Hybrid_Multi_Lane_Spatial_Logic/regular/Regular_Sensors.thy
The file was modified thys/Hybrid_Systems_VCs/HS_VC_Examples.thy
The file was modified thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_ndfun.thy
The file was modified thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_rel.thy
The file was modified thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_ndfun.thy
The file was modified thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_rel.thy
The file was modified thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT_Examples.thy
The file was modified thys/HyperCTL/Finite_Noninterference.thy
The file was modified thys/IMAP-CRDT/IMAP-proof-independent.thy
The file was modified thys/IMP2/basic/Semantics.thy
The file was modified thys/IP_Addresses/Prefix_Match.thy
The file was modified thys/Impossible_Geometry/Impossible_Geometry.thy
The file was modified thys/Inductive_Inference/Universal.thy
The file was modified thys/Interval_Arithmetic_Word32/Finite_String.thy
The file was modified thys/Interval_Arithmetic_Word32/Interval_Word32.thy
The file was modified thys/Iptables_Semantics/Semantics_Embeddings.thy
The file was modified thys/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy
The file was modified thys/Irrational_Series_Erdos_Straus/Irrational_Series_Erdos_Straus.thy
The file was modified thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy
The file was modified thys/IsaGeoCoq/Tarski_Neutral.thy
The file was modified thys/Isabelle_Marries_Dirac/Deutsch_Jozsa.thy
The file was modified thys/Isabelle_Marries_Dirac/Measurement.thy
The file was modified thys/Isabelle_Marries_Dirac/Quantum_Teleportation.thy
The file was modified thys/Jacobson_Basic_Algebra/Group_Theory.thy
The file was modified thys/KAD/Antidomain_Semiring.thy
The file was modified thys/KAT_and_DRA/SingleSorted/Test_Dioid.thy
The file was modified thys/KAT_and_DRA/TwoSorted/DRAT2.thy
The file was modified thys/Kleene_Algebra/Dioid_Models.thy
The file was modified thys/Kleene_Algebra/Kleene_Algebra_Models.thy
The file was modified thys/Knot_Theory/Example.thy
The file was modified thys/Knot_Theory/Kauffman_Matrix.thy
The file was modified thys/Koenigsberg_Friendship/KoenigsbergBridge.thy
The file was modified thys/Koenigsberg_Friendship/MoreGraph.thy
The file was modified thys/Kruskal/Kruskal_Misc.thy
The file was modified thys/Kuratowski_Closure_Complement/KuratowskiClosureComplementTheorem.thy
The file was modified thys/LLL_Basis_Reduction/Gram_Schmidt_Int.thy
The file was modified thys/LLL_Factorization/LLL_Factorization.thy
The file was modified thys/LLL_Factorization/Missing_Dvd_Int_Poly.thy
The file was modified thys/LOFT/LinuxRouter_OpenFlow_Translation.thy
The file was modified thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy
The file was modified thys/LTL_Master_Theorem/LTL_to_DRA/Transition_Functions.thy
The file was modified thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy
The file was modified thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy
The file was modified thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy
The file was modified thys/LTL_to_DRA/Logical_Characterization.thy
The file was modified thys/LTL_to_DRA/Mojmir.thy
The file was modified thys/LTL_to_DRA/Semi_Mojmir.thy
The file was modified thys/Launchbury/Env.thy
The file was modified thys/Launchbury/Nominal-Utils.thy
The file was modified thys/LinearQuantifierElim/Thys/FRE.thy
The file was modified thys/Linear_Programming/Matrix_LinPoly.thy
The file was modified thys/Linear_Recurrences/Rational_FPS_Solver.thy
The file was modified thys/List-Index/List_Index.thy
The file was modified thys/LocalLexing/Derivations.thy
The file was modified thys/LocalLexing/Ladder.thy
The file was modified thys/LocalLexing/PathLemmas.thy
The file was modified thys/LocalLexing/TheoremD14.thy
The file was modified thys/LocalLexing/TheoremD5.thy
The file was modified thys/LocalLexing/Validity.thy
The file was modified thys/Localization_Ring/Localization.thy
The file was modified thys/Lp/Functional_Spaces.thy
The file was modified thys/Lucas_Theorem/Lucas_Theorem.thy
The file was modified thys/MFMC_Countable/MFMC_Unbounded.thy
The file was modified thys/MFMC_Countable/Matrix_For_Marginals.thy
The file was modified thys/MFOTL_Monitor/Table.thy
The file was modified thys/MSO_Regex_Equivalence/Pi_Regular_Exp_Dual.thy
The file was modified thys/Matrices_for_ODEs/MTX_Flows.thy
The file was modified thys/Matrices_for_ODEs/MTX_Preliminaries.thy
The file was modified thys/Matrix_Tensor/Matrix_Tensor.thy
The file was modified thys/Metalogic_ProofChecker/Logic.thy
The file was modified thys/Metalogic_ProofChecker/Name.thy
The file was modified thys/Metalogic_ProofChecker/SortsExe.thy
The file was modified thys/Metalogic_ProofChecker/Term_Subst.thy
The file was modified thys/Modal_Logics_for_NTS/FL_Formula.thy
The file was modified thys/Modal_Logics_for_NTS/FL_Validity.thy
The file was modified thys/Modal_Logics_for_NTS/Formula.thy
The file was modified thys/Modal_Logics_for_NTS/L_Transform.thy
The file was modified thys/Modal_Logics_for_NTS/Residual.thy
The file was modified thys/Modal_Logics_for_NTS/S_Transform.thy
The file was modified thys/Modal_Logics_for_NTS/Transition_System.thy
The file was modified thys/Modal_Logics_for_NTS/Weak_Transition_System.thy
The file was modified thys/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy
The file was modified thys/Modular_arithmetic_LLL_and_HNF_algorithms/Storjohann.thy
The file was modified thys/Modular_arithmetic_LLL_and_HNF_algorithms/Uniqueness_Hermite_JNF.thy
The file was modified thys/Monad_Memo_DP/example/Bellman_Ford.thy
The file was modified thys/MonoBoolTranAlgebra/Statements.thy
The file was modified thys/Multi_Party_Computation/Malicious_OT.thy
The file was modified thys/Multirelations/Multirelations.thy
The file was modified thys/Nested_Multisets_Ordinals/Duplicate_Free_Multiset.thy
The file was modified thys/Network_Security_Policy_Verification/TopoS_Helper.thy
The file was modified thys/Network_Security_Policy_Verification/TopoS_Stateful_Policy.thy
The file was modified thys/Neumann_Morgenstern_Utility/Neumann_Morgenstern_Utility_Theorem.thy
The file was modified thys/Octonions/Cross_Product_7.thy
The file was modified thys/Optics/Lens_Order.thy
The file was modified thys/Optics/Scenes.thy
The file was modified thys/Order_Lattice_Props/Fixpoint_Fusion.thy
The file was modified thys/Order_Lattice_Props/Galois_Connections.thy
The file was modified thys/Order_Lattice_Props/Order_Lattice_Props.thy
The file was modified thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy
The file was modified thys/Order_Lattice_Props/Order_Lattice_Props_Wenzel.thy
The file was modified thys/Order_Lattice_Props/Representations.thy
The file was modified thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy
The file was modified thys/Ordinal_Partitions/Erdos_Milner.thy
The file was modified thys/Ordinal_Partitions/Library_Additions.thy
The file was modified thys/Ordinal_Partitions/Omega_Omega.thy
The file was modified thys/Ordinary_Differential_Equations/IVP/Cones.thy
The file was modified thys/Ordinary_Differential_Equations/IVP/Flow.thy
The file was modified thys/Ordinary_Differential_Equations/Library/Linear_ODE.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy
The file was modified thys/PAC_Checker/PAC_More_Poly.thy
The file was modified thys/PAC_Checker/PAC_Specification.thy
The file was modified thys/PLM/TAO_5_MetaSolver.thy
The file was modified thys/Padic_Ints/Cring_Poly.thy
The file was modified thys/Padic_Ints/Function_Ring.thy
The file was modified thys/Padic_Ints/Hensels_Lemma.thy
The file was modified thys/Padic_Ints/Padic_Integers.thy
The file was modified thys/Padic_Ints/Zp_Compact.thy
The file was modified thys/Partial_Order_Reduction/Extensions/Set_Extensions.thy
The file was modified thys/Perfect-Number-Thm/Sigma.thy
The file was modified thys/Physical_Quantities/Power_int.thy
The file was modified thys/Planarity_Certificates/Verification/Check_Non_Planarity_Verification.thy
The file was modified thys/Poincare_Bendixson/Analysis_Misc.thy
The file was modified thys/Poincare_Bendixson/Poincare_Bendixson.thy
The file was modified thys/Poincare_Disc/Poincare_Between.thy
The file was modified thys/Poincare_Disc/Poincare_Tarski.thy
The file was modified thys/Polynomial_Factorization/Missing_List.thy
The file was modified thys/Polynomials/MPoly_PM.thy
The file was modified thys/Polynomials/MPoly_Type_Class.thy
The file was modified thys/Polynomials/MPoly_Type_Class_Ordered.thy
The file was modified thys/Polynomials/More_MPoly_Type.thy
The file was modified thys/Prim_Dijkstra_Simple/Directed_Graph_Specs.thy
The file was modified thys/Progress_Tracking/Exchange.thy
The file was modified thys/Progress_Tracking/Exchange_Abadi.thy
The file was modified thys/Projective_Geometry/Desargues_2D.thy
The file was modified thys/Projective_Measurements/CHSH_Inequality.thy
The file was modified thys/Propositional_Proof_Systems/CNF_Formulas.thy
The file was modified thys/Propositional_Proof_Systems/HC_Compl_Consistency.thy
The file was modified thys/Propositional_Proof_Systems/Resolution_Compl_Consistency.thy
The file was modified thys/QHLProver/Matrix_Limit.thy
The file was modified thys/QR_Decomposition/Least_Squares_Approximation.thy
The file was modified thys/QR_Decomposition/Miscellaneous_QR.thy
The file was modified thys/QR_Decomposition/QR_Decomposition.thy
The file was modified thys/QR_Decomposition/QR_Efficient.thy
The file was modified thys/Quantales/Dioid_Models_New.thy
The file was modified thys/Quantales/Quantale_Left_Sided.thy
The file was modified thys/Quantales/Quantale_Modules.thy
The file was modified thys/Quantales/Quantales.thy
The file was modified thys/Quantales/Quantic_Nuclei_Conuclei.thy
The file was modified thys/Rank_Nullity_Theorem/Mod_Type.thy
The file was modified thys/Real_Impl/Real_Unique_Impl.thy
The file was modified thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heapmap.thy
The file was modified thys/Refine_Imperative_HOL/IICF/Impl/IICF_Array_Matrix.thy
The file was modified thys/RefinementReactive/Refinement.thy
The file was modified thys/Regex_Equivalence/Deriv_Autos.thy
The file was modified thys/Regular-Sets/pEquivalence_Checking.thy
The file was modified thys/Regular_Algebras/Regular_Algebra_Models.thy
The file was modified thys/Regular_Algebras/Regular_Algebras.thy
The file was modified thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy
The file was modified thys/Relational_Minimum_Spanning_Trees/Kruskal.thy
The file was modified thys/Relational_Minimum_Spanning_Trees/Prim.thy
The file was modified thys/Relational_Paths/Path_Algorithms.thy
The file was modified thys/Residuated_Lattices/Residuated_Boolean_Algebras.thy
The file was modified thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy
The file was modified thys/SC_DOM_Components/Core_DOM_DOM_Components.thy
The file was modified thys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy
The file was modified thys/SC_DOM_Components/Shadow_DOM_SC_DOM_Components.thy
The file was modified thys/SIFUM_Type_Systems/Compositionality.thy
The file was modified thys/SIFUM_Type_Systems/LocallySoundModeUse.thy
The file was modified thys/SIFUM_Type_Systems/Preliminaries.thy
The file was modified thys/SIFUM_Type_Systems/TypeSystem.thy
The file was modified thys/Safe_Distance/Safe_Distance_Reaction.thy
The file was modified thys/Shadow_DOM/Shadow_DOM.thy
The file was modified thys/Shadow_DOM/monads/ShadowRootMonad.thy
The file was modified thys/Shadow_SC_DOM/Shadow_DOM.thy
The file was modified thys/Sigma_Commit_Crypto/Chaum_Pedersen_Sigma_Commit.thy
The file was modified thys/Sigma_Commit_Crypto/Okamoto_Sigma_Commit.thy
The file was modified thys/Sigma_Commit_Crypto/Rivest.thy
The file was modified thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy
The file was modified thys/Smith_Normal_Form/Cauchy_Binet.thy
The file was modified thys/Smith_Normal_Form/Diagonal_To_Smith.thy
The file was modified thys/Smith_Normal_Form/Elementary_Divisor_Rings.thy
The file was modified thys/Smith_Normal_Form/Finite_Field_Mod_Type_Connection.thy
The file was modified thys/Smith_Normal_Form/Rings2_Extended.thy
The file was modified thys/Smith_Normal_Form/SNF_Algorithm.thy
The file was modified thys/Smith_Normal_Form/SNF_Algorithm_Euclidean_Domain.thy
The file was modified thys/Smooth_Manifolds/Projective_Space.thy
The file was modified thys/Sort_Encodings/G.thy
The file was modified thys/Sort_Encodings/M.thy
The file was modified thys/Sort_Encodings/T.thy
The file was modified thys/Source_Coding_Theorem/Source_Coding_Theorem.thy
The file was modified thys/Stable_Matching/Sotomayor.thy
The file was modified thys/Stable_Matching/Strategic.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/More_Unification.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy
The file was modified thys/Stone_Algebras/Stone_Construction.thy
The file was modified thys/Stone_Kleene_Relation_Algebras/Kleene_Relation_Algebras.thy
The file was modified thys/Stone_Kleene_Relation_Algebras/Matrix_Kleene_Algebras.thy
The file was modified thys/Stone_Relation_Algebras/Fixpoints.thy
The file was modified thys/Stone_Relation_Algebras/Linear_Order_Matrices.thy
The file was modified thys/Stone_Relation_Algebras/Matrix_Relation_Algebras.thy
The file was modified thys/Stone_Relation_Algebras/Relation_Algebras.thy
The file was modified thys/Stone_Relation_Algebras/Relation_Subalgebras.thy
The file was modified thys/Sturm_Tarski/Sturm_Tarski.thy
The file was modified thys/Subset_Boolean_Algebras/Subset_Boolean_Algebras.thy
The file was modified thys/SuperCalc/superposition.thy
The file was modified thys/Syntax_Independent_Logic/Deduction_Q.thy
The file was modified thys/Syntax_Independent_Logic/Syntax.thy
The file was modified thys/Syntax_Independent_Logic/Syntax_Arith.thy
The file was modified thys/Timed_Automata/DBM_Operations.thy
The file was modified thys/Topological_Semantics/ex_LFUs.thy
The file was modified thys/Topological_Semantics/topo_operators_basic.thy
The file was modified thys/Transformer_Semantics/Isotone_Transformers.thy
The file was modified thys/Transformer_Semantics/Kleisli_Transformers.thy
The file was modified thys/Transformer_Semantics/Powerset_Monad.thy
The file was modified thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy
The file was modified thys/Tree_Decomposition/Graph.thy
The file was modified thys/Twelvefold_Way/Equiv_Relations_on_Functions.thy
The file was modified thys/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy
The file was modified thys/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy
The file was modified thys/UTP/toolkit/List_Extra.thy
The file was modified thys/UTP/toolkit/Map_Extra.thy
The file was modified thys/UTP/utp/utp_concurrency.thy
The file was modified thys/UTP/utp/utp_rel_laws.thy
The file was modified thys/UTP/utp/utp_rel_opsem.thy
The file was modified thys/UTP/utp/utp_subst.thy
The file was modified thys/UTP/utp/utp_var.thy
The file was modified thys/VectorSpace/LinearCombinations.thy
The file was modified thys/Vickrey_Clarke_Groves/Argmax.thy
The file was modified thys/Vickrey_Clarke_Groves/MiscTools.thy
The file was modified thys/Vickrey_Clarke_Groves/SetUtils.thy
The file was modified thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy
The file was modified thys/Vickrey_Clarke_Groves/Universes.thy
The file was modified thys/WHATandWHERE_Security/Parallel_Composition.thy
The file was modified thys/WOOT_Strong_Eventual_Consistency/IntegrateInsertCommute.thy
The file was modified thys/WOOT_Strong_Eventual_Consistency/Psi.thy
The file was modified thys/WOOT_Strong_Eventual_Consistency/StrongConvergence.thy
The file was modified thys/WebAssembly/Wasm_Checker_Types.thy
The file was modified thys/WebAssembly/Wasm_Properties.thy
The file was modified thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy
The file was modified thys/Winding_Number_Eval/Missing_Transcendental.thy
The file was modified thys/Winding_Number_Eval/Winding_Number_Eval.thy
The file was modified thys/Word_Lib/More_Word_Operations.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/ZFC_in_HOL/ZFC_in_HOL.thy
Changeset 11905:805ab069d5b3 by fabian huch _huch@in.tum.de_:
merged
Changeset 11904:869efd0ea35a by fabian huch _huch@in.tum.de_:
jenkins: pre/post-hook results
The file was modified admin/jenkins/ci_build_afp.scala
The file was modified admin/jenkins/ci_build_all.scala
The file was modified admin/jenkins/ci_build_mac.scala
The file was modified admin/jenkins/ci_build_slow.scala
The file was modified admin/jenkins/ci_build_testboard.scala
Changeset 11903:00b5c6a1f1dd by yonoteam _jonjulian23@gmail.com_:
changed to opaque_lifiting as suggested by Isabelle/Jenkins
The file was modified thys/Hybrid_Systems_VCs/HS_VC_Examples.thy
The file was modified thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_rel.thy
The file was modified thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT_Examples.thy
The file was modified thys/Matrices_for_ODEs/MTX_Flows.thy
The file was modified thys/Matrices_for_ODEs/MTX_Preliminaries.thy
Changeset 11902:f6308605d678 by yonoteam _jonjulian23@gmail.com_:
changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins
The file was modified thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_ndfun.thy
Changeset 11901:9c417896a51d by manuel eberl _eberlm@in.tum.de_:
Added missing Public_Announcement_Logic to ROOTS file
The file was modified thys/ROOTS
Changeset 11900:9070c70617f5 by Burkhart Wolff _wolff@lri.fr_:
More Support on Clean Syntax, Basic Lens Support, New Examples.
The file was addedthys/Clean/examples/IsPrime.thy
The file was addedthys/Clean/examples/LinearSearch.thy
The file was addedthys/Clean/examples/Quicksort.thy
The file was addedthys/Clean/src/Lens_Laws.thy
The file was addedthys/Clean/src/Optics.thy
The file was modified thys/Clean/ROOT
The file was modified thys/Clean/document/root.tex
The file was modified thys/Clean/examples/Quicksort_concept.thy
The file was modified thys/Clean/examples/SquareRoot_concept.thy
The file was modified thys/Clean/src/Clean.thy
The file was modified thys/Clean/src/Clean_Main.thy
The file was modified thys/Clean/src/Clean_Symbex.thy
The file was modified thys/Clean/src/Hoare_Clean.thy
The file was modified thys/Clean/src/Hoare_MonadSE.thy
The file was modified thys/Clean/src/MonadSE.thy
The file was modified thys/Clean/src/Symbex_MonadSE.thy
The file was modified thys/Clean/src/Test_Clean.thy
Changeset 11899:2ccc185fdaac by paulson _lp15@cam.ac.uk_:
finishing arg -&gt; Arg and moving some material out of Stirling_Formula/Gamma_Asymptotics
The file was modified thys/Complex_Geometry/More_Complex.thy
The file was modified thys/Perron_Frobenius/Roots_Unity.thy
The file was modified thys/Stirling_Formula/Gamma_Asymptotics.thy