equal
deleted
inserted
replaced
14 (*old-style theory syntax*) |
14 (*old-style theory syntax*) |
15 use "thy_syntax.ML"; |
15 use "thy_syntax.ML"; |
16 |
16 |
17 use "hologic.ML"; |
17 use "hologic.ML"; |
18 |
18 |
19 use "~~/src/Provers/simplifier.ML"; |
|
20 use "~~/src/Provers/splitter.ML"; |
19 use "~~/src/Provers/splitter.ML"; |
21 use "~~/src/Provers/hypsubst.ML"; |
20 use "~~/src/Provers/hypsubst.ML"; |
22 use "~~/src/Provers/induct_method.ML"; |
21 use "~~/src/Provers/induct_method.ML"; |
23 use "~~/src/Provers/make_elim.ML"; |
22 use "~~/src/Provers/make_elim.ML"; |
24 use "~~/src/Provers/classical.ML"; |
23 use "~~/src/Provers/classical.ML"; |