Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid persistence of static context: instantiation arguments should provide proper dynamic context;
  2. more antiquotations;
  3. more markup;
  4. clarified name, syntax, messages;
  5. more antiquotations;
  6. more control symbols;
  7. tuned signature;
  8. ML antiquotations to instantiate types/terms/props;
Changeset 74573:e2e2bc1f9570 by wenzelm:
avoid persistence of static context: instantiation arguments should provide proper dynamic context;
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
Changeset 74572:08b4292abe2b by wenzelm:
more antiquotations;
The file was modified src/HOL/Analysis/normarith.ML (diff)
Changeset 74571:d3e36521fcc7 by wenzelm:
more markup;
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/Syntax/syntax_phases.ML (diff)
Changeset 74570:7625b5d7cfe2 by wenzelm:
clarified name, syntax, messages;
The file was modified etc/symbols (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/HOL/Decision_Procs/langford.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
Changeset 74569:f4613ca298e6 by wenzelm:
more antiquotations;
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/HOL/Decision_Procs/langford.ML (diff)
Changeset 74568:7f311d474cf9 by wenzelm:
more control symbols;
The file was modified etc/symbols (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)
Changeset 74567:40910c47d7a1 by wenzelm:
tuned signature;
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML (diff)
The file was modified src/Pure/Isar/keyword.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/Isar/parse.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/Thy/document_marker.ML (diff)
Changeset 74566:8e0f0317e266 by wenzelm:
ML antiquotations to instantiate types/terms/props;
The file was modified src/Pure/Isar/keyword.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)