Summary
- unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
- tuned signature -- suppress pointless exports;
- tuned;
- more standard pretty printing; tuned messages;
- tuned;
- tuned whitespace; tuned comments;
The file was modified | src/HOL/Library/code_test.ML (diff) |
The file was modified | src/HOL/ROOT (diff) |
The file was modified | src/HOL/Library/code_test.ML (diff) |
The file was modified | src/HOL/Library/code_test.ML (diff) |
The file was modified | src/HOL/Library/code_test.ML (diff) |
The file was modified | src/HOL/Library/Code_Test.thy (diff) |
The file was modified | src/HOL/Library/code_test.ML (diff) |
The file was modified | src/HOL/Library/code_test.ML (diff) |