Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Added tag Isabelle2023-RC2 for changeset 53b59fa42696
  2. prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
  3. revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion);
  4. output panel: don't discard already filtered messages
  5. merged
  6. tuned signature: more operations;
  7. avoid excessive accumulation of garbage, for profiling of huge sessions;
  8. clarified signature: systematic use of Properties.make_string;
  9. tuned;
  10. support for let in Alethe name bindings;
  11. merged
  12. A few more cosmetic changes to proofs
  13. merged
  14. tidying a few proofs a bit more
  15. partly tidied some truly horrible proofs
Changeset 78470:67bf692cf1ab by wenzelm:
Added tag Isabelle2023-RC2 for changeset 53b59fa42696
The file was modified .hgtags (diff)
Changeset 78469:53b59fa42696 by wenzelm:
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
The file was modified NEWS (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/Isar/proof_display.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/ex/Guess.thy (diff)
Changeset 78468:33bc244eafdb by wenzelm:
revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion);
The file was modified src/Tools/jEdit/src/output_dockable.scala (diff)
Changeset 78467:ab9cc7cda0ec by kleing:
output panel: don't discard already filtered messages
The file was modified src/Tools/jEdit/src/output_dockable.scala (diff)
Changeset 78466:1a68cd0c57d3 by wenzelm:
merged
Changeset 78465:4dffc47b7e91 by wenzelm:
tuned signature: more operations;
The file was modified src/HOL/Library/conditional_parametricity.ML (diff)
The file was modified src/Pure/Isar/proof_display.ML (diff)
Changeset 78464:12af46f2cd94 by wenzelm:
avoid excessive accumulation of garbage, for profiling of huge sessions;
The file was modified src/Pure/context.ML (diff)
Changeset 78463:c956b43749f0 by wenzelm:
clarified signature: systematic use of Properties.make_string;
The file was modified src/Pure/PIDE/markup.ML (diff)
Changeset 78462:3023063833e4 by wenzelm:
tuned;
The file was modified src/Pure/Thy/bibtex.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
Changeset 78461:71713dd09c35 by mathias fleury _mathias.fleury@mpi-inf.mpg.de_:
support for let in Alethe name bindings;
The file was modified src/HOL/Tools/SMT/smt_solver.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_proof.ML (diff)
Changeset 78460:0bd81d528598 by paulson:
merged
Changeset 78459:51b8f6a19978 by paulson _lp15@cam.ac.uk_:
A few more cosmetic changes to proofs
The file was modified src/HOL/Analysis/Polytope.thy (diff)
Changeset 78458:b221d12978ee by paulson:
merged
Changeset 78457:e2a5c4117ff0 by paulson _lp15@cam.ac.uk_:
tidying a few proofs a bit  more
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
Changeset 78456:57f5127d2ff2 by paulson _lp15@cam.ac.uk_:
partly tidied some truly horrible proofs
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)