equal
deleted
inserted
replaced
6 header {* The basis of Higher-Order Logic *} |
6 header {* The basis of Higher-Order Logic *} |
7 |
7 |
8 theory HOL |
8 theory HOL |
9 imports CPure |
9 imports CPure |
10 uses |
10 uses |
11 "~~/src/Tools/integer.ML" |
|
12 ("hologic.ML") |
11 ("hologic.ML") |
13 "~~/src/Tools/IsaPlanner/zipper.ML" |
12 "~~/src/Tools/IsaPlanner/zipper.ML" |
14 "~~/src/Tools/IsaPlanner/isand.ML" |
13 "~~/src/Tools/IsaPlanner/isand.ML" |
15 "~~/src/Tools/IsaPlanner/rw_tools.ML" |
14 "~~/src/Tools/IsaPlanner/rw_tools.ML" |
16 "~~/src/Tools/IsaPlanner/rw_inst.ML" |
15 "~~/src/Tools/IsaPlanner/rw_inst.ML" |