diff -r cbd32a0f2f41 -r 74be52691d62 src/HOLCF/ex/Dagstuhl.ML
--- a/src/HOLCF/ex/Dagstuhl.ML	Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/ex/Dagstuhl.ML	Thu Jun 29 16:28:40 1995 +0200
@@ -1,52 +1,49 @@
-(*
 (* $Id$ *)
-*)
-
 
 open Dagstuhl;
 
-val YS_def2  = fix_prover Dagstuhl.thy  YS_def  "YS  = scons[y][YS]";
-val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]";
+val YS_def2  = fix_prover2 Dagstuhl.thy  YS_def  "YS = scons`y`YS";
+val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = scons`y`(scons`y`YYS)";
 
 
-val prems = goal Dagstuhl.thy "YYS << scons[y][YYS]";
-by (rtac (YYS_def RS ssubst) 1);
+val prems = goal Dagstuhl.thy "YYS << scons`y`YYS";
+by (rewrite_goals_tac [YYS_def]);
 by (rtac fix_ind 1);
 by (resolve_tac adm_thms 1);
-by (contX_tacR 1);
+by (cont_tacR 1);
 by (rtac minimal 1);
 by (rtac (beta_cfun RS ssubst) 1);
-by (contX_tacR 1);
+by (cont_tacR 1);
 by (rtac monofun_cfun_arg 1);
 by (rtac monofun_cfun_arg 1);
 by (atac 1);
-qed "lemma3";
+val lemma3 = result();
 
-val prems = goal Dagstuhl.thy "scons[y][YYS] << YYS";
+val prems = goal Dagstuhl.thy "scons`y`YYS << YYS";
 by (rtac (YYS_def2 RS ssubst) 1);
 back();
 by (rtac monofun_cfun_arg 1);
 by (rtac lemma3 1);
-qed "lemma4";
+val lemma4=result();
 
 (* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
 
-val prems = goal Dagstuhl.thy "scons[y][YYS] = YYS";
+val prems = goal Dagstuhl.thy "scons`y`YYS = YYS";
 by (rtac antisym_less 1);
 by (rtac lemma4 1);
 by (rtac lemma3 1);
-qed "lemma5";
+val lemma5=result();
 
 val prems = goal Dagstuhl.thy "YS = YYS";
 by (rtac stream_take_lemma 1);
 by (nat_ind_tac "n" 1);
 by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
-by (res_inst_tac [("y1","y")] (YS_def2 RS ssubst) 1);
-by (res_inst_tac [("y1","y")] (YYS_def2 RS ssubst) 1);
+by (rtac (YS_def2 RS ssubst) 1);
+by (rtac (YYS_def2 RS ssubst) 1);
 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
 by (rtac (lemma5 RS sym RS subst) 1);
 by (rtac refl 1);
-qed "wir_moel";
+val wir_moel=result();
 
 (* ------------------------------------------------------------------------ *)
 (* Zweite L"osung: Bernhard M"oller                                         *)
@@ -55,95 +52,24 @@
 (* ------------------------------------------------------------------------ *)
 
 val prems = goal Dagstuhl.thy "YYS << YS";
-by (rtac (YYS_def RS ssubst) 1);
+by (rewrite_goals_tac [YYS_def]);
 by (rtac fix_least 1);
 by (rtac (beta_cfun RS ssubst) 1);
-by (contX_tacR 1);
+by (cont_tacR 1);
 by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
-qed "lemma6";
+val lemma6=result();
 
 val prems = goal Dagstuhl.thy "YS << YYS";
-by (rtac (YS_def RS ssubst) 1);
+by (rewrite_goals_tac [YS_def]);
 by (rtac fix_ind 1);
 by (resolve_tac adm_thms 1);
-by (contX_tacR 1);
+by (cont_tacR 1);
 by (rtac minimal 1);
 by (rtac (beta_cfun RS ssubst) 1);
-by (contX_tacR 1);
-by (res_inst_tac [("y2","y10")] (lemma5 RS sym RS ssubst) 1);
+by (cont_tacR 1);
+by (rtac (lemma5 RS sym RS ssubst) 1);
 by (etac monofun_cfun_arg 1);
-qed "lemma7";
+val lemma7 = result();
 
 val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
 
-
-(* ------------------------------------------------------------------------ *)
-(* L"osung aus Dagstuhl (F.R.)                                              *)
-(* Wie oben, jedoch ohne Konstantendefinition f"ur YS, YYS                  *)
-(* ------------------------------------------------------------------------ *)
-
-val prems = goal Stream2.thy
-    "(fix[LAM x. scons[y][x]]) = scons[y][fix[LAM x. scons[y][x]]]";
-by (rtac (fix_eq RS ssubst) 1);
-back();
-back();
-by (rtac (beta_cfun RS ssubst) 1);
-by (contX_tacR 1);
-by (rtac refl 1);
-qed "lemma1";
-
-val prems = goal Stream2.thy
-    "(fix[ LAM z. scons[y][scons[y][z]]]) = \
-\     scons[y][scons[y][(fix[ LAM z. scons[y][scons[y][z]]])]]";
-by (rtac (fix_eq RS ssubst) 1);
-back();
-back();
-by (rtac (beta_cfun RS ssubst) 1);
-by (contX_tacR 1);
-by (rtac refl 1);
-qed "lemma2";
-
-val prems = goal Stream2.thy
-"fix[LAM z. scons[y][scons[y][z]]] << \
-\ scons[y][fix[LAM z. scons[y][scons[y][z]]]]";
-by (rtac fix_ind 1);
-by (resolve_tac adm_thms 1);
-by (contX_tacR 1);
-by (rtac minimal 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
-by (rtac monofun_cfun_arg 1);
-by (rtac monofun_cfun_arg 1);
-by (atac 1);
-qed "lemma3";
-
-val prems = goal Stream2.thy
-" scons[y][fix[LAM z. scons[y][scons[y][z]]]] <<\
-\ fix[LAM z. scons[y][scons[y][z]]]";
-by (rtac (lemma2 RS ssubst) 1);
-back();
-by (rtac monofun_cfun_arg 1);
-by (rtac lemma3 1);
-qed "lemma4";
-
-val prems = goal Stream2.thy
-" scons[y][fix[LAM z. scons[y][scons[y][z]]]] =\
-\ fix[LAM z. scons[y][scons[y][z]]]";
-by (rtac antisym_less 1);
-by (rtac lemma4 1);
-by (rtac lemma3 1);
-qed "lemma5";
-
-val prems = goal Stream2.thy
-    "(fix[LAM x. scons[y][x]]) = (fix[ LAM z. scons[y][scons[y][z]]])";
-by (rtac stream_take_lemma 1);
-by (nat_ind_tac "n" 1);
-by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
-by (rtac (lemma1 RS ssubst) 1);
-by (rtac (lemma2 RS ssubst) 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
-by (rtac (lemma5 RS sym RS subst) 1);
-by (rtac refl 1);
-qed "wir_moel";
-
-
-