changeset 4041 | 4df7f385fe9f |
parent 4010 | 59cac65fb751 |
child 4122 | f63c283cefaf |
4040:20f7471eedbf | 4041:4df7f385fe9f |
---|---|
13 print_depth 1; |
13 print_depth 1; |
14 |
14 |
15 use_thy "HOLCF"; |
15 use_thy "HOLCF"; |
16 |
16 |
17 (* sections axioms, ops *) |
17 (* sections axioms, ops *) |
18 |
|
19 use "ax_ops/holcflogic.ML"; |
18 use "ax_ops/holcflogic.ML"; |
20 use "ax_ops/thy_axioms.ML"; |
19 use "ax_ops/thy_axioms.ML"; |
21 use "ax_ops/thy_ops.ML"; |
20 use "ax_ops/thy_ops.ML"; |
22 use "ax_ops/thy_syntax.ML"; |
21 use "ax_ops/thy_syntax.ML"; |
23 |
22 |