Skip to content
Success

Changes

Summary

  1. clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
  2. tuned;
  3. tuned;
Changeset 69216:1a52baa70aed by wenzelm:
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
The file was modified NEWS (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Eisbach/Tests.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/HOLCF/Cfun.thy (diff)
The file was modified src/HOL/HOLCF/ex/Pattern_Match.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Syntax.thy (diff)
The file was modified src/HOL/Library/Code_Abstract_Nat.thy (diff)
The file was modified src/HOL/Library/Code_Lazy.thy (diff)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/ex/Cartouche_Examples.thy (diff)
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/isar_cmd.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/ML/ml_context.ML (diff)
The file was modified src/Pure/Tools/ghc.ML (diff)
Changeset 69215:ab94035ba6ea by wenzelm:
tuned;
The file was modified src/HOL/List.thy (diff)
Changeset 69214:74455459973d by wenzelm:
tuned;
The file was modified src/HOL/Decision_Procs/Cooper.thy (diff)
The file was modified src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy (diff)