| changeset 1301 | 42782316d510 |
| parent 1296 | ae31bb7774a7 |
| child 1338 | d2fc3bfaee7f |
| 1300:c7a8f374339b | 1301:42782316d510 |
|---|---|
9 |
9 |
10 val banner = "Higher-Order Logic with curried functions"; |
10 val banner = "Higher-Order Logic with curried functions"; |
11 writeln banner; |
11 writeln banner; |
12 |
12 |
13 print_depth 1; |
13 print_depth 1; |
14 set eta_contract; |
|
15 |
14 |
16 (* Add user sections *) |
15 (* Add user sections *) |
17 use "../Pure/section_utils.ML"; |
16 use "../Pure/section_utils.ML"; |
18 use "thy_syntax.ML"; |
17 use "thy_syntax.ML"; |
19 |
18 |