Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. A few new lemmas plus some refinements
  2. merged
  3. produced Mirabelle output directly in ML until Scala output gets fixed
  4. clarified signature;
  5. clarified signature;
  6. clarified signature;
  7. removed unused material (left-over from fd0c85d7da38);
  8. support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);
  9. removed junk;
  10. merged
  11. separated commands from annotations to be able to abstract about the latter only
  12. prefer standard Term.dest_abs, with minor deviation of generated names;
  13. tuned comments;
  14. more examples
  15. workaround for old macOS versions, after change of Let's Encrypt root certificate --- see also https://letsencrypt.org/docs/dst-root-ca-x3-expiration-september-2021 --- Java/Scala Isabelle_System.download() works, but curl doens't;
  16. more complete simp rules
  17. more complete simp rules
  18. avoid overaggressive contraction of conversions
  19. normalizing NOT (numeral _) (again)
Changeset 74513:67d87d224e00 by paulson _lp15@cam.ac.uk_:
A few new lemmas plus some refinements
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.thy
The file was modified src/HOL/Analysis/Complex_Transcendental.thy
The file was modified src/HOL/Analysis/Elementary_Topology.thy
The file was modified src/HOL/Analysis/Polytope.thy
The file was modified src/HOL/Limits.thy
Changeset 74512:c434f4e74947 by desharna:
merged
Changeset 74511:6d111935299c by desharna:
produced Mirabelle output directly in ML until Scala output gets fixed
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML
Changeset 74510:21a20b990724 by wenzelm:
clarified signature;
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
The file was modified src/Pure/Isar/proof.ML
The file was modified src/Tools/try.ML
Changeset 74509:f24ade4ff3cc by wenzelm:
clarified signature;
The file was modified src/HOL/Library/refute.ML
The file was modified src/HOL/Tools/Nunchaku/nunchaku.ML
The file was modified src/Pure/Isar/element.ML
The file was modified src/Pure/logic.ML
The file was modified src/Pure/raw_simplifier.ML
The file was modified src/Pure/thm.ML
Changeset 74508:3315c551fe6e by wenzelm:
clarified signature;
The file was modified src/HOL/Tools/Nitpick/nitpick_commands.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
The file was modified src/HOL/Tools/try0.ML
The file was modified src/Tools/quickcheck.ML
The file was modified src/Tools/solve_direct.ML
The file was modified src/Tools/try.ML
Changeset 74507:a241eadc0e3f by wenzelm:
removed unused material (left-over from fd0c85d7da38);
The file was modified src/Tools/try.ML
Changeset 74506:d97c48dc87fa by wenzelm:
support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);
The file was modified src/HOL/Hoare/hoare_tac.ML
Changeset 74505:ce8152fb021b by wenzelm:
removed junk;
The file was modified src/HOL/Hoare/ExamplesTC.thy
Changeset 74504:7422950f3955 by nipkow:
merged
Changeset 74503:403ce50e6a2a by nipkow:
separated commands from annotations to be able to abstract about the latter only
The file was modified src/HOL/Hoare/ExamplesTC.thy
The file was modified src/HOL/Hoare/Hoare_Logic.thy
The file was modified src/HOL/Hoare/Hoare_Logic_Abort.thy
The file was modified src/HOL/Hoare/Hoare_Syntax.thy
The file was modified src/HOL/Hoare/SchorrWaite.thy
The file was modified src/HOL/Hoare/hoare_syntax.ML
The file was modified src/HOL/Hoare/hoare_tac.ML
Changeset 74502:907483081d4c by wenzelm:
prefer standard Term.dest_abs, with minor deviation of generated names;
The file was modified src/HOL/Tools/Meson/meson_clausify.ML
Changeset 74501:0803dd7f920d by wenzelm:
tuned comments;
The file was modified src/HOL/Tools/Meson/meson.ML
The file was modified src/HOL/Tools/Meson/meson_clausify.ML
Changeset 74500:40f03761f77f by nipkow:
more examples
The file was modified src/HOL/IMP/Hoare_Total_EX.thy
The file was modified src/HOL/IMP/Hoare_Total_EX2.thy
The file was modified src/HOL/IMP/VCG_Total_EX2.thy
Changeset 74499:059743bc8311 by wenzelm:
workaround for old macOS versions, after change of Let's Encrypt root certificate --- see also https://letsencrypt.org/docs/dst-root-ca-x3-expiration-september-2021 --- Java/Scala Isabelle_System.download() works, but curl doens't;
The file was modified lib/Tools/components
Changeset 74498:27475e64a887 by haftmann:
more complete simp rules
The file was modified src/HOL/Bit_Operations.thy
The file was modified src/HOL/Library/Word.thy
Changeset 74497:9c04a82c3128 by haftmann:
more complete simp rules
The file was modified src/HOL/Bit_Operations.thy
Changeset 74496:807b094a9b78 by haftmann:
avoid overaggressive contraction of conversions
The file was modified NEWS
The file was modified src/HOL/Library/Word.thy
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/F.thy
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
Changeset 74495:bc27c490aaac by haftmann:
normalizing NOT (numeral _) (again)
The file was modified NEWS
The file was modified src/HOL/Bit_Operations.thy

Summary

  1. Simplified a definition
  2. modify propa
  3. bit singleton shifts recovered for the sake of backward compatibility
  4. updated to 7422950f3955
  5. merge
  6. EPO: simplify proof
  7. primer
  8. more complete simp rules
  9. more complete simp rules (examples)
  10. avoid overaggressive contraction of conversions
  11. slightly more prominence for proof tools; more examples
Changeset 12091:70694297a67c by paulson _lp15@cam.ac.uk_:
Simplified a definition
The file was modified thys/Ordinal_Partitions/Omega_Omega.thy
Changeset 12090:96920cdaac55 by nanjiang _nanjiang@whu.edu.cn_:
modify propa
The file was modified thys/Dominance_CHK/Dom_Kildall.thy
The file was modified thys/Dominance_CHK/Dom_Kildall_Property.thy
The file was modified thys/Dominance_CHK/Sorted_Less2.thy
Changeset 12089:b29e73d246d4 by haftmann:
bit singleton shifts recovered for the sake of backward compatibility
The file was addedthys/Word_Lib/Singleton_Bit_Shifts.thy
The file was modified thys/Word_Lib/Bitwise.thy
The file was modified thys/Word_Lib/Guide.thy
The file was modified thys/Word_Lib/Legacy_Aliases.thy
The file was modified thys/Word_Lib/Reversed_Bit_Lists.thy
The file was modified thys/Word_Lib/Word_Lib_Sumo.thy
Changeset 12088:8d2f2c35b69d by nipkow:
updated to 7422950f3955
The file was modified thys/Case_Labeling/Examples/Hoare/Labeled_Hoare.thy
The file was modified thys/Case_Labeling/Examples/Hoare/labeled_hoare_tac.ML
The file was modified thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy
Changeset 12087:7a7acbc421da by alexander bentkamp _a.bentkamp@vu.nl_:
merge
Changeset 12086:8fda5e92692f by alexander bentkamp _a.bentkamp@vu.nl_:
EPO: simplify proof
The file was modified thys/Lambda_Free_EPO/Lambda_Free_EPO.thy
Changeset 12085:134b70fc858e by haftmann:
primer
The file was modified thys/Word_Lib/Guide.thy
Changeset 12084:f8dc7663c3cf by haftmann:
more complete simp rules
The file was modified thys/Word_Lib/Examples.thy
The file was modified thys/Word_Lib/More_Word.thy
Changeset 12083:052886ce16c0 by haftmann:
more complete simp rules (examples)
The file was modified thys/Word_Lib/Examples.thy
Changeset 12082:c42c2c2447c2 by haftmann:
avoid overaggressive contraction of conversions
The file was modified thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy
The file was modified thys/CAVA_LTL_Modelchecker/SM/RefPoint/SM_State.thy
The file was modified thys/Complx/ex/SumArr.thy
The file was modified thys/IEEE_Floating_Point/Conversion_IEEE_Float.thy
The file was modified thys/Iptables_Semantics/Common/Word_Upto.thy
The file was modified thys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/PAC_Checker/PAC_Checker_Relation.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy
The file was modified thys/Word_Lib/Aligned.thy
The file was modified thys/Word_Lib/More_Word.thy
The file was modified thys/Word_Lib/More_Word_Operations.thy
The file was modified thys/Word_Lib/Rsplit.thy
The file was modified thys/Word_Lib/Word_32.thy
The file was modified thys/Word_Lib/Word_64.thy
The file was modified thys/Word_Lib/Word_8.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
Changeset 12081:721d0f625e02 by haftmann:
slightly more prominence for proof tools; more examples
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was modified thys/Word_Lib/Examples.thy
The file was modified thys/Word_Lib/Guide.thy