| changeset 5210 | 54aaa779b6b4 |
| parent 4222 | d7573d6d0513 |
| child 6260 | a8010d459ef7 |
| 5209:a69fe5a61b6c | 5210:54aaa779b6b4 |
|---|---|
8 *) |
8 *) |
9 |
9 |
10 val banner = "Constructive Type Theory"; |
10 val banner = "Constructive Type Theory"; |
11 writeln banner; |
11 writeln banner; |
12 |
12 |
13 reset global_names; |
|
14 |
|
15 print_depth 1; |
13 print_depth 1; |
16 |
14 |
17 use_thy "CTT"; |
15 use_thy "CTT"; |
18 use "$ISABELLE_HOME/src/Provers/typedsimp.ML"; |
16 use "$ISABELLE_HOME/src/Provers/typedsimp.ML"; |
19 use "rew.ML"; |
17 use "rew.ML"; |