changeset 4024 | 3c056eab237c |
parent 3981 | b4f93a8da835 |
child 4088 | 9be9e39fd862 |
4023:a9dc0484c903 | 4024:3c056eab237c |
---|---|
7 Should be executed in the subdirectory HOL. |
7 Should be executed in the subdirectory HOL. |
8 *) |
8 *) |
9 |
9 |
10 val banner = "Higher-Order Logic"; |
10 val banner = "Higher-Order Logic"; |
11 writeln banner; |
11 writeln banner; |
12 |
|
13 reset global_names; |
|
14 |
12 |
15 print_depth 1; |
13 print_depth 1; |
16 |
14 |
17 (* Add user sections *) |
15 (* Add user sections *) |
18 use "../Pure/section_utils.ML"; |
16 use "../Pure/section_utils.ML"; |