Skip to content
Aborted

Changes

Summary

  1. merged
  2. recovered printing of DIM('a) (cf. 899c9c4e4a4c);
  3. updated;
  4. simplified syntax;
  5. clarified syntax category names according to Isabelle/ML/Scala;
  6. simplified syntax: Parse.term corresponds to Args.term etc.;
  7. clarified syntax categories;
  8. cartouche abbreviations work both for " as well;
Changeset 63142:4cf6726eb85e by wenzelm:
merged
Changeset 63141:7e5084ad95aa by wenzelm:
recovered printing of DIM('a) (cf. 899c9c4e4a4c);
The file was modified src/HOL/Multivariate_Analysis/Euclidean_Space.thy (diff)
Changeset 63140:0644c2e5a989 by wenzelm:
updated;
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
Changeset 63139:d905741a80e8 by wenzelm:
simplified syntax;
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
The file was modified src/Pure/Isar/parse.ML (diff)
Changeset 63138:70f4d67235a0 by wenzelm:
clarified syntax category names according to Isabelle/ML/Scala;
The file was modified src/Doc/Isar_Ref/Document_Preparation.thy (diff)
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
Changeset 63137:9553f11d67c4 by wenzelm:
simplified syntax: Parse.term corresponds to Args.term etc.;
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
The file was modified src/Pure/Isar/parse.ML (diff)
Changeset 63136:fd11a538daac by wenzelm:
clarified syntax categories;
The file was modified src/HOL/Tools/Nitpick/nitpick_commands.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
Changeset 63135:035785035a1a by wenzelm:
cartouche abbreviations work both for " as well;
The file was modified NEWS (diff)
The file was modified src/Pure/General/completion.scala (diff)