equal
deleted
inserted
replaced
11 |
11 |
12 use "hologic.ML"; |
12 use "hologic.ML"; |
13 |
13 |
14 use "~~/src/Provers/splitter.ML"; |
14 use "~~/src/Provers/splitter.ML"; |
15 use "~~/src/Provers/hypsubst.ML"; |
15 use "~~/src/Provers/hypsubst.ML"; |
|
16 use "~~/src/Provers/IsaPlanner/zipper.ML"; |
|
17 use "~~/src/Provers/IsaPlanner/isand.ML"; |
|
18 use "~~/src/Provers/IsaPlanner/rw_tools.ML"; |
|
19 use "~~/src/Provers/IsaPlanner/rw_inst.ML"; |
16 use "~~/src/Provers/eqsubst.ML"; |
20 use "~~/src/Provers/eqsubst.ML"; |
17 use "~~/src/Provers/induct_method.ML"; |
21 use "~~/src/Provers/induct_method.ML"; |
18 use "~~/src/Provers/classical.ML"; |
22 use "~~/src/Provers/classical.ML"; |
19 use "~~/src/Provers/blast.ML"; |
23 use "~~/src/Provers/blast.ML"; |
20 use "~~/src/Provers/clasimp.ML"; |
24 use "~~/src/Provers/clasimp.ML"; |