Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. tuned signature: more exports;
  3. clarified signature: prefer internal Thm_Name.T over external Facts.ref;
  4. more robust / permissive;
  5. clarified signature: more operations;
  6. tuned;
  7. clarified operations, following pretty_thm_name;
  8. more accurate treatment of Thm_Name.T;
  9. renamed lemmas
  10. merged
  11. renamed theorems
  12. renamed theorems
Changeset 80332:4bed658a01fc by wenzelm:
merged
Changeset 80331:6f25a035069c by wenzelm:
tuned signature: more exports;
The file was modified src/Pure/Tools/find_theorems.ML
Changeset 80330:e01aae620437 by wenzelm:
clarified signature: prefer internal Thm_Name.T over external Facts.ref;
The file was modified src/Pure/Tools/find_theorems.ML
The file was modified src/Pure/thm_name.ML
Changeset 80329:d90a96894644 by wenzelm:
more robust / permissive;
The file was modified src/Pure/Isar/proof_context.ML
Changeset 80328:559909bd7715 by wenzelm:
clarified signature: more operations;
The file was modified src/HOL/Library/code_test.ML
The file was modified src/HOL/SPARK/Tools/spark_vcs.ML
The file was modified src/HOL/Tools/Nitpick/nitpick.ML
The file was modified src/Pure/General/pretty.ML
The file was modified src/Pure/Isar/proof_context.ML
The file was modified src/Pure/Isar/proof_display.ML
The file was modified src/Pure/Tools/find_theorems.ML
The file was modified src/Pure/unify.ML
The file was modified src/Tools/Code/code_target.ML
Changeset 80327:e4e643705d90 by wenzelm:
tuned;
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
Changeset 80326:53f12ab896e6 by wenzelm:
clarified operations, following pretty_thm_name;
The file was modified src/Pure/Isar/proof_context.ML
Changeset 80325:dca37c6479e3 by wenzelm:
more accurate treatment of Thm_Name.T;
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
Changeset 80324:a6d5de03ffeb by desharna:
renamed lemmas
The file was modified NEWS
The file was modified src/HOL/Library/Multiset.thy
The file was modified src/HOL/Library/Multiset_Order.thy
Changeset 80323:5e5dcebd1ed8 by desharna:
merged
Changeset 80322:b10f7c981df6 by desharna:
renamed theorems
The file was modified NEWS
The file was modified src/HOL/Fun_Def.thy
The file was modified src/HOL/Library/Multiset.thy
The file was modified src/HOL/MicroJava/DFA/Kildall.thy
The file was modified src/HOL/Tools/Function/function_core.ML
The file was modified src/HOL/Wellfounded.thy
Changeset 80321:31b9dfbe534c by desharna:
renamed theorems
The file was modified NEWS
The file was modified src/HOL/Wellfounded.thy

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

Summary

  1. merged
  2. more accurate treatment of Thm_Name.T; more accurate facts_space via Proof_Context.facts_of_fact;
  3. more accurate treatment of Thm_Name.T; more standard string_of_int;
  4. adapted to Isabelle/e01aae620437;
  5. eliminate odd clone;
  6. eliminate clone, following Isabelle/6f25a035069c;
  7. tuned: more direct Long_Name.base_name;
  8. adapted to Isabelle/e01aae620437;
  9. more accurate treatment of Thm_Name.T; tuned output;
  10. tuned signature;
  11. adapted to Isabelle/a6d5de03ffeb
  12. adapted (again) to Isabelle/b10f7c981df6
  13. adapted to Isabelle/b10f7c981df6
  14. adapted to Isabelle/31b9dfbe534c
Changeset 14464:c90b2c7f278f by wenzelm:
merged
Changeset 14463:6a2f4d2f766f by wenzelm:
more accurate treatment of Thm_Name.T;<br>more accurate facts_space via Proof_Context.facts_of_fact;
The file was modified thys/AutoCorres2/lib/ml-helpers/utils.ML
Changeset 14462:95d2e49007e0 by wenzelm:
more accurate treatment of Thm_Name.T;<br>more standard string_of_int;
The file was modified thys/AutoCorres2/lib/Basic_Runs_To_VCG.thy
Changeset 14461:3585ab9577b7 by wenzelm:
adapted to Isabelle/e01aae620437;
The file was modified thys/Proof_Strategy_Language/Utils.ML
Changeset 14460:ad215c72fdd3 by wenzelm:
eliminate odd clone;
The file was modified thys/AutoCorres2/exception_rewrite.ML
The file was modified thys/AutoCorres2/monad_convert.ML
The file was modified thys/AutoCorres2/type_strengthen.ML
The file was modified thys/AutoCorres2/utils.ML
Changeset 14459:66b98537a422 by wenzelm:
eliminate clone, following Isabelle/6f25a035069c;
The file was modified thys/AutoCorres2/utils.ML
Changeset 14458:55ddf8aa974c by wenzelm:
tuned: more direct Long_Name.base_name;
The file was modified thys/AOT/AOT_commands.ML
Changeset 14457:7950997d3ae5 by wenzelm:
adapted to Isabelle/e01aae620437;
The file was modified thys/AOT/AOT_commands.ML
The file was modified thys/AutoCorres2/lib/Apply_Trace.thy
The file was modified thys/AutoCorres2/lib/ml-helpers/ThmExtras.ML
Changeset 14456:801a8094878c by wenzelm:
more accurate treatment of Thm_Name.T;<br>tuned output;
The file was modified thys/Planarity_Certificates/l4v/lib/wp/WP-method.ML
Changeset 14455:49be21395d3c by wenzelm:
tuned signature;
The file was modified thys/Planarity_Certificates/l4v/lib/wp/WP-method.ML
Changeset 14454:aa4958cf6b67 by desharna:
adapted to Isabelle/a6d5de03ffeb
The file was modified thys/Given_Clause_Loops/Fair_DISCOUNT_Loop.thy
The file was modified thys/Given_Clause_Loops/Fair_Zipperposition_Loop.thy
The file was modified thys/Given_Clause_Loops/Fair_iProver_Loop.thy
The file was modified thys/Saturation_Framework_Extensions/Standard_Redundancy_Criterion.thy
Changeset 14453:ea1fed26dc6f by desharna:
adapted (again) to Isabelle/b10f7c981df6
The file was modified thys/Dict_Construction/transfer_termination.ML
The file was modified thys/JinjaThreads/Framework/FWLTS.thy
Changeset 14452:f106ca7d4cec by desharna:
adapted to Isabelle/b10f7c981df6
The file was modified thys/ADS_Functor/Generic_ADS_Construction.thy
The file was modified thys/AWN/AWN_Cterms.thy
The file was modified thys/Coinductive/Coinductive_List.thy
The file was modified thys/Complete_Non_Orders/Well_Relations.thy
The file was modified thys/ConcurrentHOL/Aczel_Sequences.thy
The file was modified thys/ConcurrentHOL/HOL_Basis.thy
The file was modified thys/ConcurrentHOL/Next_Imp.thy
The file was modified thys/Constructive_Cryptography/Distinguisher.thy
The file was modified thys/CryptHOL/Misc_CryptHOL.thy
The file was modified thys/Dict_Construction/Dict_Construction.thy
The file was modified thys/Free-Groups/Cancelation.thy
The file was modified thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy
The file was modified thys/Functional_Ordered_Resolution_Prover/Weighted_FO_Ordered_Resolution_Prover.thy
The file was modified thys/Given_Clause_Loops/Fair_DISCOUNT_Loop.thy
The file was modified thys/Given_Clause_Loops/Fair_Otter_Loop_Def.thy
The file was modified thys/Given_Clause_Loops/Fair_Zipperposition_Loop.thy
The file was modified thys/Given_Clause_Loops/Fair_iProver_Loop.thy
The file was modified thys/Groebner_Bases/Confluence.thy
The file was modified thys/HereditarilyFinite/Rank.thy
The file was modified thys/HoareForDivergence/DivLogicCompleteness.thy
The file was modified thys/HoareForDivergence/DivLogicSoundness.thy
The file was modified thys/HoareForDivergence/StdLogicCompleteness.thy
The file was modified thys/HoareForDivergence/StdLogicSoundness.thy
The file was modified thys/HyperHoareLogic/TotalLogic.thy
The file was modified thys/JinjaThreads/Basic/Auxiliary.thy
The file was modified thys/JinjaThreads/Common/SemiType.thy
The file was modified thys/JinjaThreads/Common/WellForm.thy
The file was modified thys/JinjaThreads/Compiler/Correctness1.thy
The file was modified thys/JinjaThreads/Compiler/Correctness2.thy
The file was modified thys/JinjaThreads/Compiler/J0Bisim.thy
The file was modified thys/JinjaThreads/Compiler/JVMJ1.thy
The file was modified thys/JinjaThreads/Framework/Bisimulation.thy
The file was modified thys/JinjaThreads/Framework/FWLTS.thy
The file was modified thys/JinjaThreads/Framework/LTS.thy
The file was modified thys/JinjaThreads/MM/JMM_Spec.thy
The file was modified thys/Khovanskii_Theorem/Khovanskii.thy
The file was modified thys/Lambda_Free_EPO/Lambda_Free_EPO.thy
The file was modified thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy
The file was modified thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy
The file was modified thys/Lambda_Free_KBOs/Lambda_Free_TKBO_Coefs.thy
The file was modified thys/Lambda_Free_RPOs/Extension_Orders.thy
The file was modified thys/Lambda_Free_RPOs/Infinite_Chain.thy
The file was modified thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy
The file was modified thys/Lambda_Free_RPOs/Lambda_Free_RPOs.thy
The file was modified thys/Lambda_Free_RPOs/Lambda_Free_Util.thy
The file was modified thys/Open_Induction/Restricted_Predicates.thy
The file was modified thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
The file was modified thys/Ordered_Resolution_Prover/Lazy_List_Chain.thy
The file was modified thys/Partial_Order_Reduction/Ample_Abstract.thy
The file was modified thys/Polynomials/MPoly_Type_Class_Ordered.thy
The file was modified thys/Polynomials/Power_Products.thy
The file was modified thys/Polynomials/Utils.thy
The file was modified thys/Possibilistic_Noninterference/Language_Semantics.thy
The file was modified thys/Saturation_Framework/Given_Clause_Architectures.thy
The file was modified thys/Saturation_Framework_Extensions/Standard_Redundancy_Criterion.thy
The file was modified thys/Simple_Clause_Learning/SCL_FOL.thy
The file was modified thys/Simple_Clause_Learning/Termination.thy
The file was modified thys/Simple_Clause_Learning/Trail_Induced_Ordering.thy
The file was modified thys/Substitutions_Lambda_Free/Substitutions_Lambda_Free.thy
The file was modified thys/TESL_Language/Hygge_Theory.thy
The file was modified thys/VeriComp/Lifting_Simulation_To_Bisimulation.thy
The file was modified thys/VeriComp/Simulation.thy
The file was modified thys/VeriComp/Well_founded.thy
The file was modified thys/WOOT_Strong_Eventual_Consistency/Consistency.thy
The file was modified thys/WOOT_Strong_Eventual_Consistency/CreateConsistent.thy
The file was modified thys/WOOT_Strong_Eventual_Consistency/Example.thy
The file was modified thys/WOOT_Strong_Eventual_Consistency/IntegrateInsertCommute.thy
The file was modified thys/Well_Quasi_Orders/Almost_Full.thy
The file was modified thys/ZFC_in_HOL/ZFC_Cardinals.thy
Changeset 14451:6d2644467fcb by desharna:
adapted to Isabelle/31b9dfbe534c
The file was modified thys/Dict_Construction/Dict_Construction.thy
The file was modified thys/Dict_Construction/Documentation/Termination.thy