Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
  2. tuned signature -- suppress pointless exports;
  3. tuned;
  4. more standard pretty printing; tuned messages;
  5. tuned;
  6. tuned whitespace; tuned comments;
Changeset 64582:3d20ded18f14 by wenzelm:
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 64581:ee4b9cea7fb5 by wenzelm:
tuned signature -- suppress pointless exports;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 64580:43ad19fbe9dc by wenzelm:
tuned;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 64579:38a1d8b41189 by wenzelm:
more standard pretty printing;<br>tuned messages;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 64578:7b20f9f94f4e by wenzelm:
tuned;
The file was modified src/HOL/Library/Code_Test.thy (diff)
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 64577:0288a566c966 by wenzelm:
tuned whitespace;<br>tuned comments;
The file was modified src/HOL/Library/code_test.ML (diff)