Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. material on finite maps
  3. more uniform cartouche syntax; more documentation;
  4. more uniform cartouche syntax;
  5. more robust exit: avoid later Consolidate_Execution with handle_raw_edits (cf. 2fd3a6d6ba2e);
  6. tuned message;
  7. clarified message;
  8. actually ensure globally unique counter results (amending a5853334c179);
  9. retain original PolyML.pointerEq;
  10. some modernization of notation
  11. deprecation of ASCII syntax for indexed big operators
Changeset 68811:51fdede038c9 by lars hupel _lars.hupel@mytum.de_:
merged
Changeset 68810:db97c1ed115e by lars hupel _lars.hupel@mytum.de_:
material on finite maps
The file was modified src/HOL/Library/Finite_Map.thy (diff)
Changeset 68809:f6c88cb715db by wenzelm:
more uniform cartouche syntax;<br>more documentation;
The file was modified src/Doc/Isar_Ref/Document_Preparation.thy (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
Changeset 68808:5467858e9419 by wenzelm:
more uniform cartouche syntax;
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Thy/sessions.ML (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 68807:e28978310a2a by wenzelm:
more robust exit: avoid later Consolidate_Execution with handle_raw_edits (cf. 2fd3a6d6ba2e);
The file was modified src/Pure/PIDE/session.scala (diff)
Changeset 68806:4597812d5182 by wenzelm:
tuned message;
The file was modified src/Pure/General/exn.scala (diff)
The file was modified src/Pure/System/command_line.scala (diff)
Changeset 68805:57455c561849 by wenzelm:
clarified message;
The file was modified src/Pure/PIDE/prover.scala (diff)
Changeset 68804:cbde6e3b132b by wenzelm:
actually ensure globally unique counter results (amending a5853334c179);
The file was modified src/Pure/Concurrent/counter.ML (diff)
Changeset 68803:169bf32b35dd by wenzelm:
retain original PolyML.pointerEq;
The file was modified NEWS (diff)
The file was modified src/Pure/ML_Bootstrap.thy (diff)
Changeset 68802:3974935e0252 by haftmann:
some modernization of notation
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
Changeset 68801:c898c2b1fd58 by haftmann:
deprecation of ASCII syntax for indexed big operators
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Lattices_Big.thy (diff)