equal
deleted
inserted
replaced
5 |
5 |
6 Higher-Order Logic. |
6 Higher-Order Logic. |
7 *) |
7 *) |
8 |
8 |
9 theory HOL = CPure |
9 theory HOL = CPure |
10 files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"): |
10 files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") |
|
11 ("Tools/meson.ML"): |
11 |
12 |
12 |
13 |
13 (** Core syntax **) |
14 (** Core syntax **) |
14 |
15 |
15 global |
16 global |
219 use "simpdata.ML" setup Simplifier.setup |
220 use "simpdata.ML" setup Simplifier.setup |
220 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup |
221 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup |
221 setup Splitter.setup setup Clasimp.setup setup iff_attrib_setup |
222 setup Splitter.setup setup Clasimp.setup setup iff_attrib_setup |
222 setup attrib_setup |
223 setup attrib_setup |
223 |
224 |
|
225 use "Tools/meson.ML" |
|
226 |
224 end |
227 end |