# HG changeset patch # User oheimb # Date 878217453 -3600 # Node ID 4df7f385fe9faaeac50a99588a2d65753a9cd7f7 # Parent 20f7471eedbf094c19d262e6cfd9dbe8d8cf301f domain package: * theorems are stored in the theory * creates hierachical name space * minor changes to some names and values (for consistency), e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas * separator between mutual domain definitions changed from "," to "and" * minor debugging of Domain_Library.mk_var_names diff -r 20f7471eedbf -r 4df7f385fe9f src/HOLCF/ROOT.ML --- a/src/HOLCF/ROOT.ML Thu Oct 30 11:43:32 1997 +0100 +++ b/src/HOLCF/ROOT.ML Thu Oct 30 14:17:33 1997 +0100 @@ -15,7 +15,6 @@ use_thy "HOLCF"; (* sections axioms, ops *) - use "ax_ops/holcflogic.ML"; use "ax_ops/thy_axioms.ML"; use "ax_ops/thy_ops.ML";