# HG changeset patch
# User mueller
# Date 873796460 -7200
# Node ID 1ea4a45b9412e8902f09cf7f4c5856957f042e85
# Parent  5c9d3a63e9ffd1d2a8f49c4b266c299730bbb837
moved extended adm_tac to new place

diff -r 5c9d3a63e9ff -r 1ea4a45b9412 src/HOLCF/Fix.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)));
diff -r 5c9d3a63e9ff -r 1ea4a45b9412 src/HOLCF/HOLCF.ML
--- 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;
diff -r 5c9d3a63e9ff -r 1ea4a45b9412 src/HOLCF/Lift.ML
--- 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";
 (* ---------------------------------------------------------- *)