minor changes due to more powerful continuity check in Lift3.ML
authormueller
Thu, 24 Apr 1997 17:35:47 +0200
changeset 3032 74c5f175aa8e
parent 3031 c51ee445605d
child 3033 50e14d6d894f
minor changes due to more powerful continuity check in Lift3.ML
src/HOLCF/ex/Dagstuhl.ML
--- a/src/HOLCF/ex/Dagstuhl.ML	Thu Apr 24 17:04:07 1997 +0200
+++ b/src/HOLCF/ex/Dagstuhl.ML	Thu Apr 24 17:35:47 1997 +0200
@@ -9,9 +9,8 @@
 val prems = goal Dagstuhl.thy "YYS << y && YYS";
 by (rtac (YYS_def RS def_fix_ind) 1);
 by (Simp_tac 1);
-by (cont_tacR 1);
-by (stac beta_cfun 1);
-by (cont_tacR 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
 by (rtac monofun_cfun_arg 1);
 by (rtac monofun_cfun_arg 1);
 by (atac 1);
@@ -60,9 +59,8 @@
 val prems = goal Dagstuhl.thy "YS << YYS";
 by (rtac (YS_def RS def_fix_ind) 1);
 by (Simp_tac 1);
-by (cont_tacR 1);
-by (stac beta_cfun 1);
-by (cont_tacR 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
 by (stac (lemma5 RS sym) 1);
 by (etac monofun_cfun_arg 1);
 val lemma7 = result();