equal
deleted
inserted
replaced
5 header {* Intuitionistic first-order logic *} |
5 header {* Intuitionistic first-order logic *} |
6 |
6 |
7 theory IFOL |
7 theory IFOL |
8 imports Pure |
8 imports Pure |
9 uses |
9 uses |
|
10 "~~/src/Tools/misc_legacy.ML" |
10 "~~/src/Provers/splitter.ML" |
11 "~~/src/Provers/splitter.ML" |
11 "~~/src/Provers/hypsubst.ML" |
12 "~~/src/Provers/hypsubst.ML" |
12 "~~/src/Tools/IsaPlanner/zipper.ML" |
13 "~~/src/Tools/IsaPlanner/zipper.ML" |
13 "~~/src/Tools/IsaPlanner/isand.ML" |
14 "~~/src/Tools/IsaPlanner/isand.ML" |
14 "~~/src/Tools/IsaPlanner/rw_tools.ML" |
15 "~~/src/Tools/IsaPlanner/rw_tools.ML" |