changeset 4122 | f63c283cefaf |
parent 4041 | 4df7f385fe9f |
child 4128 | 42584a53a3e7 |
--- a/src/HOLCF/ROOT.ML Tue Nov 04 14:37:51 1997 +0100 +++ b/src/HOLCF/ROOT.ML Tue Nov 04 14:40:29 1997 +0100 @@ -14,14 +14,10 @@ use_thy "HOLCF"; -(* sections axioms, ops *) -use "ax_ops/holcflogic.ML"; -use "ax_ops/thy_axioms.ML"; -use "ax_ops/thy_ops.ML"; -use "ax_ops/thy_syntax.ML"; +use "HOLCFLogic"; +use "contconsts"; -(* sections domain, generated *) - +(* domain package *) use "domain/library.ML"; use "domain/syntax.ML"; use "domain/axioms.ML";