# HG changeset patch
# User mueller
# Date 861896147 -7200
# Node ID 74c5f175aa8e7c3f33c5e4862b407b10ab35462c
# Parent  c51ee445605da14c65f6da087420afc4021d9e46
minor changes due to more powerful continuity check in Lift3.ML

diff -r c51ee445605d -r 74c5f175aa8e 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();