equal
deleted
inserted
replaced
11 val banner = "ZF Set Theory (in FOL)"; |
11 val banner = "ZF Set Theory (in FOL)"; |
12 writeln banner; |
12 writeln banner; |
13 |
13 |
14 reset eta_contract; |
14 reset eta_contract; |
15 |
15 |
16 print_depth 1; |
|
17 |
|
18 (*syntax for old-style theory sections*) |
16 (*syntax for old-style theory sections*) |
19 use "thy_syntax"; |
17 use "thy_syntax"; |
20 |
18 |
21 with_path "Integ" use_thy "Main_ZFC"; |
19 with_path "Integ" use_thy "Main_ZFC"; |
22 |
20 |
23 print_depth 8; |
|
24 |
|
25 Goal "True"; (*leave subgoal package empty*) |
21 Goal "True"; (*leave subgoal package empty*) |