Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. tuned;
  2. merged
  3. added command 'ML_export';
  4. more examples;
  5. tuned output;
  6. pretty-print according to defaults of input syntax;
  7. more accurate diagram;
  8. proper output;
  9. treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
Changeset 68278:23e12da0866c by wenzelm:
tuned;
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
Changeset 68277:c2b227b8e361 by wenzelm:
merged
Changeset 68276:cbee43ff4ceb by wenzelm:
added command 'ML_export';
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 68275:b5d0318757f0 by wenzelm:
more examples;
The file was modified src/Doc/System/Environment.thy (diff)
Changeset 68274:867bd42b3f59 by wenzelm:
tuned output;
The file was modified src/Pure/Isar/element.ML (diff)
Changeset 68273:53788963c4dc by wenzelm:
pretty-print according to defaults of input syntax;
The file was modified src/Pure/Syntax/mixfix.ML (diff)
Changeset 68272:ddeb6847451a by wenzelm:
more accurate diagram;
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
Changeset 68271:77f6fa78b6e1 by wenzelm:
proper output;
The file was modified src/Pure/Syntax/mixfix.ML (diff)
Changeset 68270:2bc921b2159b by haftmann:
treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
The file was modified src/HOL/Decision_Procs/MIR.thy (diff)
The file was modified src/HOL/GCD.thy (diff)