moved extended adm_tac to new place
authormueller
Tue, 09 Sep 1997 11:14:20 +0200
changeset 3661 1ea4a45b9412
parent 3660 5c9d3a63e9ff
child 3662 4be700757406
moved extended adm_tac to new place
src/HOLCF/Fix.ML
src/HOLCF/HOLCF.ML
src/HOLCF/Lift.ML
--- 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";
 (* ---------------------------------------------------------- *)