src/HOLCF/HOLCF.ML
changeset 3661 1ea4a45b9412
parent 2355 ee9bdbe2ac8a
child 4098 71e05eb27fb6
--- 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;