--- 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();