equal
deleted
inserted
replaced
9 val banner = "Higher-Order Logic"; |
9 val banner = "Higher-Order Logic"; |
10 writeln banner; |
10 writeln banner; |
11 |
11 |
12 use "hologic.ML"; |
12 use "hologic.ML"; |
13 |
13 |
14 use "~~/src/Pure/General/hashtable.ML"; |
|
15 use "~~/src/Provers/splitter.ML"; |
14 use "~~/src/Provers/splitter.ML"; |
16 use "~~/src/Provers/hypsubst.ML"; |
15 use "~~/src/Provers/hypsubst.ML"; |
17 use "~~/src/Provers/induct_method.ML"; |
16 use "~~/src/Provers/induct_method.ML"; |
18 use "~~/src/Provers/make_elim.ML"; |
17 use "~~/src/Provers/make_elim.ML"; |
19 use "~~/src/Provers/classical.ML"; |
18 use "~~/src/Provers/classical.ML"; |