equal
deleted
inserted
replaced
9 val banner = "Pure Isabelle"; |
9 val banner = "Pure Isabelle"; |
10 val version = "Isabelle repository version"; (*filled in automatically!*) |
10 val version = "Isabelle repository version"; (*filled in automatically!*) |
11 |
11 |
12 |
12 |
13 print_depth 10; |
13 print_depth 10; |
14 error_depth 30; |
|
15 |
14 |
16 (*fake hiding of private structures*) |
15 (*fake hiding of private structures*) |
17 structure Hidden = struct end; |
16 structure Hidden = struct end; |
18 |
17 |
19 (*basic tools*) |
18 (*basic tools*) |