Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. declare case theorems as proper code equations
  3. tuned;
  4. merged;
  5. VSCode extension for official Isabelle release;
  6. misc tuning and updates for release;
  7. more manual tests;
  8. misc tuning for release;
  9. clarified error;
  10. command-line option for include_sessions;
  11. disallow pending hyps; disallow pending shyps, with option to override the check; tuned message;
  12. disallow hyps in export; handle extra shyps as explicit sort constraints;
  13. always consolidate: allow errors in presentation;
  14. proper build_heap;
  15. avoid pending shyps in global theory facts;
  16. The unwinding number is an integer.
  17. Now based on Complex_Main, not HOL.Deriv
  18. merged
  19. Incorporating new/strengthened proofs from Library and AFP entries
  20. NEWS and CONTRIBUTORS
  21. remove trailing commas
Changeset 68550:516e81f75957 by Andreas Lochbihler:
merged
Changeset 68549:bbc742358156 by Andreas Lochbihler:
declare case theorems as proper code equations
The file was modified src/HOL/Library/code_lazy.ML (diff)
Changeset 68548:a22540ac7052 by wenzelm:
tuned;
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
Changeset 68547:549a4992222f by wenzelm:
merged;
Changeset 68546:34d732a83767 by wenzelm:
VSCode extension for official Isabelle release;
The file was modified src/Tools/VSCode/extension/README.md (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 68545:7922992c99ea by wenzelm:
misc tuning and updates for release;
The file was modified ANNOUNCE (diff)
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
Changeset 68544:8285fa53bfac by wenzelm:
more manual tests;
The file was modified Admin/Release/CHECKLIST (diff)
Changeset 68543:c87e1adb91af by wenzelm:
misc tuning for release;
The file was modified NEWS (diff)
Changeset 68542:02df6c68a8cb by wenzelm:
clarified error;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 68541:12b4b3bc585d by wenzelm:
command-line option for include_sessions;
The file was modified NEWS (diff)
The file was modified src/Doc/JEdit/JEdit.thy (diff)
The file was modified src/Doc/System/Environment.thy (diff)
The file was modified src/Pure/ML/ml_console.scala (diff)
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
The file was modified src/Tools/jEdit/src/jedit_sessions.scala (diff)
Changeset 68540:000a0e062529 by wenzelm:
disallow pending hyps;<br>disallow pending shyps, with option to override the check;<br>tuned message;
The file was modified NEWS (diff)
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
Changeset 68539:6740e3611a86 by wenzelm:
disallow hyps in export;<br>handle extra shyps as explicit sort constraints;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/drule.ML (diff)
Changeset 68538:0903c4c8b455 by wenzelm:
always consolidate: allow errors in presentation;
The file was modified src/Pure/PIDE/document.ML (diff)
Changeset 68537:0299c1dccc96 by wenzelm:
proper build_heap;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 68536:e14848001c4c by wenzelm:
avoid pending shyps in global theory facts;
The file was modified src/FOL/ex/Miniscope.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
The file was modified src/HOL/Fields.thy (diff)
The file was modified src/HOL/Metis_Examples/Big_O.thy (diff)
The file was modified src/HOL/Num.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
Changeset 68535:4d09df93d1a2 by paulson _lp15@cam.ac.uk_:
The unwinding number is an integer.
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
Changeset 68534:914e1bc7369a by paulson _lp15@cam.ac.uk_:
Now based on Complex_Main, not HOL.Deriv
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
Changeset 68533:7da59435126a by paulson:
merged
Changeset 68532:f8b98d31ad45 by paulson _lp15@cam.ac.uk_:
Incorporating new/strengthened proofs from Library and AFP entries
The file was modified CONTRIBUTORS (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Summation_Tests.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Probability/Distribution_Functions.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
Changeset 68531:7c6f812afdc4 by wenda li _wl302@cam.ac.uk_:
NEWS and CONTRIBUTORS
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
Changeset 68530:a110dcc9a4c7 by lars hupel _lars.hupel@mytum.de_:
remove trailing commas
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
The file was modified src/Pure/Tools/server.scala (diff)