Skip to content
Success

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. more realistic factor;
  2. proper trim_context;
  3. proper exception positions;
  4. proper trim_context / transfer, e.g. for Specification.definition;
  5. tuned;
  6. tuned;
  7. tuned signature: more operations;
  8. minor performance tuning: avoid append to end-of-list;
Changeset 78141:456576153249 by wenzelm:
more realistic factor;
The file was modified NEWS
Changeset 78140:90a43a9b3605 by wenzelm:
proper trim_context;
The file was modified src/Pure/Isar/code.ML
Changeset 78139:bb85bda12b8e by wenzelm:
proper exception positions;
The file was modified src/Pure/Isar/code.ML
Changeset 78138:0ea55458f867 by wenzelm:
proper trim_context / transfer, e.g. for Specification.definition;
The file was modified src/Pure/assumption.ML
Changeset 78137:9ccb1ae28f0d by wenzelm:
tuned;
The file was modified src/Pure/assumption.ML
Changeset 78136:e1bd2eb4c407 by wenzelm:
tuned;
The file was modified src/Pure/drule.ML
The file was modified src/Pure/more_thm.ML
The file was modified src/Pure/raw_simplifier.ML
Changeset 78135:db2a6f9aaa77 by wenzelm:
tuned signature: more operations;
The file was modified src/Pure/thm.ML
Changeset 78134:a11ebc8c751a by wenzelm:
minor performance tuning: avoid append to end-of-list;
The file was modified src/Pure/assumption.ML