--- a/src/HOLCF/Fix.ML Mon Sep 08 10:12:28 1997 +0200
+++ b/src/HOLCF/Fix.ML Tue Sep 09 11:14:20 1997 +0200
@@ -912,8 +912,3 @@
adm_iff];
Addsimps adm_lemmas;
-
-use"adm.ML";
-
-simpset := !simpset addSolver(fn thms =>
- (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
--- a/src/HOLCF/HOLCF.ML Mon Sep 08 10:12:28 1997 +0200
+++ b/src/HOLCF/HOLCF.ML Tue Sep 09 11:14:20 1997 +0200
@@ -6,4 +6,9 @@
open HOLCF;
+use"adm.ML";
+
+simpset := !simpset addSolver(fn thms =>
+ (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
+
val HOLCF_ss = !simpset;
--- a/src/HOLCF/Lift.ML Mon Sep 08 10:12:28 1997 +0200
+++ b/src/HOLCF/Lift.ML Tue Sep 09 11:14:20 1997 +0200
@@ -75,6 +75,8 @@
simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
+
+
(* ---------------------------------------------------------- *)
section"flift1, flift2";
(* ---------------------------------------------------------- *)