# HG changeset patch
# User wenzelm
# Date 1126036277 -7200
# Node ID ecf182ccc3ca2ea2c9b3ed138482923a45e1cdd2
# Parent  5c613b64bf0a946058088aa583d00ab74ba2f288
converted to Isar theory format;

diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/Buffer.ML
--- a/src/HOLCF/FOCUS/Buffer.ML	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer.ML	Tue Sep 06 21:51:17 2005 +0200
@@ -1,13 +1,13 @@
-(*  Title: 	HOLCF/FOCUS/Buffer.ML
+(*  Title:      HOLCF/FOCUS/Buffer.ML
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 *)
 
-val set_cong = prove_goal Set.thy "!!X. A = B ==> (x:A) = (x:B)" (K [
-	etac subst 1, rtac refl 1]);
+val set_cong = prove_goal (theory "Set") "!!X. A = B ==> (x:A) = (x:B)" (K [
+        etac subst 1, rtac refl 1]);
 
-fun B_prover s tac eqs = prove_goal thy s (fn prems => [cut_facts_tac prems 1, 
-	tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
+fun B_prover s tac eqs = prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1,
+        tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
 
 fun prove_forw  s thm     = B_prover s (dtac (thm RS iffD1)) [];
 fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;
@@ -15,74 +15,74 @@
 
 (**** BufEq *******************************************************************)
 
-val mono_BufEq_F = prove_goalw thy [mono_def, BufEq_F_def] 
-		"mono BufEq_F" (K [Fast_tac 1]);
+val mono_BufEq_F = prove_goalw (the_context ()) [mono_def, BufEq_F_def]
+                "mono BufEq_F" (K [Fast_tac 1]);
 
 val BufEq_fix = mono_BufEq_F RS (BufEq_def RS def_gfp_unfold);
 
-val BufEq_unfold = prove_goal thy "(f:BufEq) = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
-		\(!x. ? ff:BufEq. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>(ff\\<cdot>x)))" (K [
-	stac (BufEq_fix RS set_cong) 1,
-	rewtac BufEq_F_def,
-	Asm_full_simp_tac 1]);
+val BufEq_unfold = prove_goal (the_context ()) "(f:BufEq) = (!d. f\\<cdot>(Md d\\<leadsto><>) = <> & \
+                \(!x. ? ff:BufEq. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>(ff\\<cdot>x)))" (K [
+        stac (BufEq_fix RS set_cong) 1,
+        rewtac BufEq_F_def,
+        Asm_full_simp_tac 1]);
 
 val Buf_f_empty = prove_forw "f:BufEq \\<Longrightarrow> f\\<cdot><> = <>" BufEq_unfold;
 val Buf_f_d     = prove_forw "f:BufEq \\<Longrightarrow> f\\<cdot>(Md d\\<leadsto><>) = <>" BufEq_unfold;
-val Buf_f_d_req = prove_forw 
-	"f:BufEq \\<Longrightarrow> \\<exists>ff. ff:BufEq \\<and> f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x" BufEq_unfold;
+val Buf_f_d_req = prove_forw
+        "f:BufEq \\<Longrightarrow> \\<exists>ff. ff:BufEq \\<and> f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x" BufEq_unfold;
 
 
 (**** BufAC_Asm ***************************************************************)
 
-val mono_BufAC_Asm_F = prove_goalw thy [mono_def, BufAC_Asm_F_def]
-		"mono BufAC_Asm_F" (K [Fast_tac 1]);
+val mono_BufAC_Asm_F = prove_goalw (the_context ()) [mono_def, BufAC_Asm_F_def]
+                "mono BufAC_Asm_F" (K [Fast_tac 1]);
 
 val BufAC_Asm_fix = mono_BufAC_Asm_F RS (BufAC_Asm_def RS def_gfp_unfold);
 
-val BufAC_Asm_unfold = prove_goal thy "(s:BufAC_Asm) = (s = <> | (? d x. \
+val BufAC_Asm_unfold = prove_goal (the_context ()) "(s:BufAC_Asm) = (s = <> | (? d x. \
 \       s = Md d\\<leadsto>x & (x = <> | (ft\\<cdot>x = Def \\<bullet> & (rt\\<cdot>x):BufAC_Asm))))" (K [
-				stac (BufAC_Asm_fix RS set_cong) 1,
-				rewtac BufAC_Asm_F_def,
-				Asm_full_simp_tac 1]);
+                                stac (BufAC_Asm_fix RS set_cong) 1,
+                                rewtac BufAC_Asm_F_def,
+                                Asm_full_simp_tac 1]);
 
 val BufAC_Asm_empty = prove_backw "<>     :BufAC_Asm" BufAC_Asm_unfold [];
 val BufAC_Asm_d     = prove_backw "Md d\\<leadsto><>:BufAC_Asm" BufAC_Asm_unfold [];
 val BufAC_Asm_d_req = prove_backw "x:BufAC_Asm ==> Md d\\<leadsto>\\<bullet>\\<leadsto>x:BufAC_Asm"
-							   BufAC_Asm_unfold [];
+                                                           BufAC_Asm_unfold [];
 val BufAC_Asm_prefix2 = prove_forw "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm"
-							 BufAC_Asm_unfold;
+                                                         BufAC_Asm_unfold;
 
 
 (**** BBufAC_Cmt **************************************************************)
 
-val mono_BufAC_Cmt_F = prove_goalw thy [mono_def, BufAC_Cmt_F_def] 
-		"mono BufAC_Cmt_F" (K [Fast_tac 1]);
+val mono_BufAC_Cmt_F = prove_goalw (the_context ()) [mono_def, BufAC_Cmt_F_def]
+                "mono BufAC_Cmt_F" (K [Fast_tac 1]);
 
 val BufAC_Cmt_fix = mono_BufAC_Cmt_F RS (BufAC_Cmt_def RS def_gfp_unfold);
 
-val BufAC_Cmt_unfold = prove_goal thy "((s,t):BufAC_Cmt) = (!d x. \
+val BufAC_Cmt_unfold = prove_goal (the_context ()) "((s,t):BufAC_Cmt) = (!d x. \
     \(s = <>       -->      t = <>) & \
     \(s = Md d\\<leadsto><>  -->      t = <>) & \
     \(s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x, rt\\<cdot>t):BufAC_Cmt))" (K [
-	stac (BufAC_Cmt_fix RS set_cong) 1,
-	rewtac BufAC_Cmt_F_def,
-	Asm_full_simp_tac 1]);
+        stac (BufAC_Cmt_fix RS set_cong) 1,
+        rewtac BufAC_Cmt_F_def,
+        Asm_full_simp_tac 1]);
 
 val BufAC_Cmt_empty = prove_backw "f:BufEq ==> (<>, f\\<cdot><>):BufAC_Cmt"
-				BufAC_Cmt_unfold [Buf_f_empty];
+                                BufAC_Cmt_unfold [Buf_f_empty];
 
-val BufAC_Cmt_d = prove_backw "f:BufEq ==> (a\\<leadsto>\\<bottom>, f\\<cdot>(a\\<leadsto>\\<bottom>)):BufAC_Cmt" 
-				BufAC_Cmt_unfold [Buf_f_d];
+val BufAC_Cmt_d = prove_backw "f:BufEq ==> (a\\<leadsto>\\<bottom>, f\\<cdot>(a\\<leadsto>\\<bottom>)):BufAC_Cmt"
+                                BufAC_Cmt_unfold [Buf_f_d];
 
-val BufAC_Cmt_d2 = prove_forw 
+val BufAC_Cmt_d2 = prove_forw
  "(Md d\\<leadsto>\\<bottom>, f\\<cdot>(Md d\\<leadsto>\\<bottom>)):BufAC_Cmt ==> f\\<cdot>(Md d\\<leadsto>\\<bottom>) = \\<bottom>" BufAC_Cmt_unfold;
-val BufAC_Cmt_d3 = prove_forw 
+val BufAC_Cmt_d3 = prove_forw
 "(Md d\\<leadsto>\\<bullet>\\<leadsto>x, f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)):BufAC_Cmt ==> (x, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x))):BufAC_Cmt"
-							BufAC_Cmt_unfold;
+                                                        BufAC_Cmt_unfold;
 
-val BufAC_Cmt_d32 = prove_forw 
+val BufAC_Cmt_d32 = prove_forw
 "(Md d\\<leadsto>\\<bullet>\\<leadsto>x, f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)):BufAC_Cmt ==> ft\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x)) = Def d"
-							BufAC_Cmt_unfold;
+                                                        BufAC_Cmt_unfold;
 
 (**** BufAC *******************************************************************)
 
@@ -114,33 +114,33 @@
 Goalw [BufAC_def] "f\\<in>BufAC \\<Longrightarrow> \\<exists>ff\\<in>BufAC. \\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x";
 by (rtac (ex_elim_lemma RS iffD2) 1);
 by Safe_tac;
-by  (fast_tac (claset() addIs [BufAC_Cmt_d32 RS Def_maximal, 
-             monofun_cfun_arg,	BufAC_Asm_empty RS BufAC_Asm_d_req]) 1);
+by  (fast_tac (claset() addIs [BufAC_Cmt_d32 RS Def_maximal,
+             monofun_cfun_arg,  BufAC_Asm_empty RS BufAC_Asm_d_req]) 1);
 by (auto_tac (claset() addIs [BufAC_Cmt_d3, BufAC_Asm_d_req],simpset()));
 qed "BufAC_f_d_req";
 
 
 (**** BufSt *******************************************************************)
 
-val mono_BufSt_F = prove_goalw thy [mono_def, BufSt_F_def] 
-		"mono BufSt_F" (K [Fast_tac 1]);
+val mono_BufSt_F = prove_goalw (the_context ()) [mono_def, BufSt_F_def]
+                "mono BufSt_F" (K [Fast_tac 1]);
 
 val BufSt_P_fix = mono_BufSt_F RS (BufSt_P_def RS def_gfp_unfold);
 
-val BufSt_P_unfold = prove_goal thy "(h:BufSt_P) = (!s. h s\\<cdot><> = <> & \
-	 \ (!d x. h \\<currency>     \\<cdot>(Md d\\<leadsto>x)   =    h (Sd d)\\<cdot>x & \
+val BufSt_P_unfold = prove_goal (the_context ()) "(h:BufSt_P) = (!s. h s\\<cdot><> = <> & \
+         \ (!d x. h \\<currency>     \\<cdot>(Md d\\<leadsto>x)   =    h (Sd d)\\<cdot>x & \
   \   (? hh:BufSt_P. h (Sd d)\\<cdot>(\\<bullet>\\<leadsto>x)   = d\\<leadsto>(hh \\<currency>    \\<cdot>x))))" (K [
-	stac (BufSt_P_fix RS set_cong) 1,
-	rewtac BufSt_F_def,
-	Asm_full_simp_tac 1]);
+        stac (BufSt_P_fix RS set_cong) 1,
+        rewtac BufSt_F_def,
+        Asm_full_simp_tac 1]);
 
-val BufSt_P_empty = prove_forw "h:BufSt_P ==> h s     \\<cdot> <>       = <>" 
-			BufSt_P_unfold;
+val BufSt_P_empty = prove_forw "h:BufSt_P ==> h s     \\<cdot> <>       = <>"
+                        BufSt_P_unfold;
 val BufSt_P_d     = prove_forw "h:BufSt_P ==> h  \\<currency>    \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x"
-			BufSt_P_unfold;
+                        BufSt_P_unfold;
 val BufSt_P_d_req = prove_forw "h:BufSt_P ==> \\<exists>hh\\<in>BufSt_P. \
-				         \ h (Sd d)\\<cdot>(\\<bullet>   \\<leadsto>x) = d\\<leadsto>(hh \\<currency>    \\<cdot>x)"
-			BufSt_P_unfold;
+                                         \ h (Sd d)\\<cdot>(\\<bullet>   \\<leadsto>x) = d\\<leadsto>(hh \\<currency>    \\<cdot>x)"
+                        BufSt_P_unfold;
 
 
 (**** Buf_AC_imp_Eq ***********************************************************)
@@ -210,11 +210,11 @@
 
 (**** alternative (not strictly) stronger version of Buf_Eq *******************)
 
-val Buf_Eq_alt_imp_Eq = prove_goalw thy [BufEq_def,BufEq_alt_def] 
-	"BufEq_alt \\<subseteq> BufEq" (K [
-	rtac gfp_mono 1,
-	rewtac BufEq_F_def,
-	Fast_tac 1]);
+val Buf_Eq_alt_imp_Eq = prove_goalw (the_context ()) [BufEq_def,BufEq_alt_def]
+        "BufEq_alt \\<subseteq> BufEq" (K [
+        rtac gfp_mono 1,
+        rewtac BufEq_F_def,
+        Fast_tac 1]);
 
 (* direct proof of "BufEq \\<subseteq> BufEq_alt" seems impossible *)
 
@@ -224,10 +224,10 @@
 by (fast_tac (claset() addEs [BufAC_f_d, BufAC_f_d_req]) 1);
 qed "Buf_AC_imp_Eq_alt";
 
-bind_thm ("Buf_Eq_imp_Eq_alt", 
+bind_thm ("Buf_Eq_imp_Eq_alt",
   subset_trans OF [Buf_Eq_imp_AC, Buf_AC_imp_Eq_alt]);
 
-bind_thm ("Buf_Eq_alt_eq", 
+bind_thm ("Buf_Eq_alt_eq",
  subset_antisym OF [Buf_Eq_alt_imp_Eq, Buf_Eq_imp_Eq_alt]);
 
 
@@ -245,11 +245,11 @@
 
 Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt";
 by Safe_tac;
-by (EVERY'[rename_tac "f", res_inst_tac 
+by (EVERY'[rename_tac "f", res_inst_tac
         [("x","\\<lambda>s. case s of Sd d => \\<Lambda> x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
 by ( Simp_tac 1);
 by (etac weak_coinduct_image 1);
-by (rewtac BufSt_F_def); 
+by (rewtac BufSt_F_def);
 by (Simp_tac 1);
 by Safe_tac;
 by (  EVERY'[rename_tac "s", induct_tac "s"] 1);
@@ -262,6 +262,3 @@
 qed "Buf_Eq_imp_St";
 
 bind_thm ("Buf_Eq_eq_St", Buf_St_imp_Eq RS (Buf_Eq_imp_St RS subset_antisym));
-
-
-
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/Buffer.thy
--- a/src/HOLCF/FOCUS/Buffer.thy	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy	Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(*  Title: 	HOLCF/FOCUS/Buffer.thy
+(*  Title:      HOLCF/FOCUS/Buffer.thy
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 
 Formalization of section 4 of
 
@@ -20,65 +20,68 @@
 
 *)
 
-Buffer = FOCUS + 
+theory Buffer
+imports FOCUS
+begin
 
-types   D
-arities D :: type
+typedecl D
 
 datatype
 
-  M	= Md D | Mreq ("\\<bullet>")
+  M     = Md D | Mreq ("\<bullet>")
 
 datatype
 
-  State	= Sd D | Snil ("\\<currency>")
+  State = Sd D | Snil ("\<currency>")
 
 types
 
-  SPF11		= "M fstream \\<rightarrow> D fstream"
-  SPEC11	= "SPF11 set"
-  SPSF11	= "State \\<Rightarrow> SPF11"
-  SPECS11	= "SPSF11 set"
+  SPF11         = "M fstream \<rightarrow> D fstream"
+  SPEC11        = "SPF11 set"
+  SPSF11        = "State \<Rightarrow> SPF11"
+  SPECS11       = "SPSF11 set"
 
 consts
 
-  BufEq_F	:: "SPEC11 \\<Rightarrow> SPEC11"
-  BufEq		:: "SPEC11"
-  BufEq_alt	:: "SPEC11"
+  BufEq_F       :: "SPEC11 \<Rightarrow> SPEC11"
+  BufEq         :: "SPEC11"
+  BufEq_alt     :: "SPEC11"
 
-  BufAC_Asm_F	:: " (M fstream set) \\<Rightarrow> (M fstream set)"
-  BufAC_Asm	:: " (M fstream set)"
-  BufAC_Cmt_F	:: "((M fstream * D fstream) set) \\<Rightarrow> \
-\		    ((M fstream * D fstream) set)"
-  BufAC_Cmt	:: "((M fstream * D fstream) set)"
-  BufAC		:: "SPEC11"
+  BufAC_Asm_F   :: " (M fstream set) \<Rightarrow> (M fstream set)"
+  BufAC_Asm     :: " (M fstream set)"
+  BufAC_Cmt_F   :: "((M fstream * D fstream) set) \<Rightarrow>
+                    ((M fstream * D fstream) set)"
+  BufAC_Cmt     :: "((M fstream * D fstream) set)"
+  BufAC         :: "SPEC11"
 
-  BufSt_F	:: "SPECS11 \\<Rightarrow> SPECS11"
-  BufSt_P	:: "SPECS11"
-  BufSt		:: "SPEC11"
+  BufSt_F       :: "SPECS11 \<Rightarrow> SPECS11"
+  BufSt_P       :: "SPECS11"
+  BufSt         :: "SPEC11"
 
 defs
 
-  BufEq_F_def	"BufEq_F B \\<equiv> {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><>) = <> \\<and>  
-			         (\\<forall>x. \\<exists>ff\\<in>B. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x)}"
-  BufEq_def	"BufEq     \\<equiv> gfp BufEq_F"
-  BufEq_alt_def	"BufEq_alt \\<equiv> gfp (\\<lambda>B. {f. \\<forall>d. f\\<cdot>(Md d\\<leadsto><> ) = <> \\<and>
-			         (\\<exists>ff\\<in>B. (\\<forall>x. f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>x) = d\\<leadsto>ff\\<cdot>x))})"
-  BufAC_Asm_F_def "BufAC_Asm_F A \\<equiv> {s. s = <> \\<or>  
-		  (\\<exists>d x. s = Md d\\<leadsto>x \\<and> (x = <> \\<or> (ft\\<cdot>x = Def \\<bullet> \\<and> (rt\\<cdot>x)\\<in>A)))}"
-  BufAC_Asm_def	"BufAC_Asm \\<equiv> gfp BufAC_Asm_F"
+  BufEq_F_def:   "BufEq_F B \<equiv> {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and>
+                                 (\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}"
+  BufEq_def:     "BufEq     \<equiv> gfp BufEq_F"
+  BufEq_alt_def: "BufEq_alt \<equiv> gfp (\<lambda>B. {f. \<forall>d. f\<cdot>(Md d\<leadsto><> ) = <> \<and>
+                                 (\<exists>ff\<in>B. (\<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x))})"
+  BufAC_Asm_F_def: "BufAC_Asm_F A \<equiv> {s. s = <> \<or>
+                  (\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}"
+  BufAC_Asm_def: "BufAC_Asm \<equiv> gfp BufAC_Asm_F"
 
-  BufAC_Cmt_F_def "BufAC_Cmt_F C \\<equiv> {(s,t). \\<forall>d x. 
-			   (s = <>         \\<longrightarrow>     t = <>                 ) \\<and>
-			   (s = Md d\\<leadsto><>   \\<longrightarrow>     t = <>                 ) \\<and>
-			   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x \\<longrightarrow> (ft\\<cdot>t = Def d \\<and> (x,rt\\<cdot>t)\\<in>C))}"
-  BufAC_Cmt_def	"BufAC_Cmt \\<equiv> gfp BufAC_Cmt_F"
-  BufAC_def	"BufAC \\<equiv> {f. \\<forall>x. x\\<in>BufAC_Asm \\<longrightarrow> (x,f\\<cdot>x)\\<in>BufAC_Cmt}"
+  BufAC_Cmt_F_def: "BufAC_Cmt_F C \<equiv> {(s,t). \<forall>d x.
+                           (s = <>         \<longrightarrow>     t = <>                 ) \<and>
+                           (s = Md d\<leadsto><>   \<longrightarrow>     t = <>                 ) \<and>
+                           (s = Md d\<leadsto>\<bullet>\<leadsto>x \<longrightarrow> (ft\<cdot>t = Def d \<and> (x,rt\<cdot>t)\<in>C))}"
+  BufAC_Cmt_def: "BufAC_Cmt \<equiv> gfp BufAC_Cmt_F"
+  BufAC_def:     "BufAC \<equiv> {f. \<forall>x. x\<in>BufAC_Asm \<longrightarrow> (x,f\<cdot>x)\<in>BufAC_Cmt}"
 
-  BufSt_F_def	"BufSt_F H \\<equiv> {h. \\<forall>s  . h s      \\<cdot><>        = <>         \\<and>
-				 (\\<forall>d x. h \\<currency>     \\<cdot>(Md d\\<leadsto>x) = h (Sd d)\\<cdot>x \\<and>
-			        (\\<exists>hh\\<in>H. h (Sd d)\\<cdot>(\\<bullet>   \\<leadsto>x) = d\\<leadsto>(hh \\<currency>\\<cdot>x)))}"
-  BufSt_P_def	"BufSt_P \\<equiv> gfp BufSt_F"
-  BufSt_def	"BufSt \\<equiv> {f. \\<exists>h\\<in>BufSt_P. f = h \\<currency>}"
+  BufSt_F_def:   "BufSt_F H \<equiv> {h. \<forall>s  . h s      \<cdot><>        = <>         \<and>
+                                 (\<forall>d x. h \<currency>     \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and>
+                                (\<exists>hh\<in>H. h (Sd d)\<cdot>(\<bullet>   \<leadsto>x) = d\<leadsto>(hh \<currency>\<cdot>x)))}"
+  BufSt_P_def:   "BufSt_P \<equiv> gfp BufSt_F"
+  BufSt_def:     "BufSt \<equiv> {f. \<exists>h\<in>BufSt_P. f = h \<currency>}"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/Buffer_adm.ML
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(*  Title: 	HOLCF/FOCUS/Buffer_adm.ML
+(*  Title:      HOLCF/FOCUS/Buffer_adm.ML
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 *)
 
 infixr 0 y;
@@ -10,30 +10,30 @@
 Addsimps [thm "Fin_0"];
 
 val BufAC_Asm_d2 = prove_forw "a\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold;
-val BufAC_Asm_d3 = prove_forw 
+val BufAC_Asm_d3 = prove_forw
     "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
 
-val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def] 
+val BufAC_Asm_F_def3 = prove_goalw (the_context ()) [BufAC_Asm_F_def]
  "(s:BufAC_Asm_F A) = (s=<> | \
 \ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
-	Auto_tac]);
+        Auto_tac]);
 
 Goal "down_cont BufAC_Asm_F";
 by (auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Asm_F_def3]));
 qed "cont_BufAC_Asm_F";
 
-val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def] 
+val BufAC_Cmt_F_def3 = prove_goalw (the_context ()) [BufAC_Cmt_F_def]
  "((s,t):BufAC_Cmt_F C) = (!d x.\
 \   (s = <>       --> t = <>                   ) & \
 \   (s = Md d\\<leadsto><>  --> t = <>                   ) & \
 \   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
-	subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
-		   \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)"  1,
-	Asm_simp_tac 1,
-	auto_tac (claset() addIs [thm "surjectiv_scons" RS sym], simpset())]);
+        subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
+                   \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)"  1,
+        Asm_simp_tac 1,
+        auto_tac (claset() addIs [thm "surjectiv_scons" RS sym], simpset())]);
 
-val cont_BufAC_Cmt_F = prove_goal thy "down_cont BufAC_Cmt_F" (K [
-	auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
+val cont_BufAC_Cmt_F = prove_goal (the_context ()) "down_cont BufAC_Cmt_F" (K [
+        auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
 
 
 (**** adm_BufAC_Asm ***********************************************************)
@@ -44,7 +44,7 @@
 by (Clarsimp_tac 1);
 qed "BufAC_Asm_F_stream_monoP";
 
-val adm_BufAC_Asm = prove_goalw thy [BufAC_Asm_def] "adm (%x. x:BufAC_Asm)" (K [
+val adm_BufAC_Asm = prove_goalw (the_context ()) [BufAC_Asm_def] "adm (%x. x:BufAC_Asm)" (K [
 rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_monoP RS fstream_gfp_admI))1]);
 
 
@@ -72,21 +72,21 @@
 by (rtac fstream_ind2 1);
 by (simp_tac (simpset() addsimps [adm_non_BufAC_Asm]) 1);
 by   (force_tac (claset() addDs [Buf_f_empty], simpset()) 1);
-by  (force_tac (claset() addSDs [BufAC_Asm_d2] 
-		addDs [Buf_f_d] addEs [ssubst], simpset()) 1);
+by  (force_tac (claset() addSDs [BufAC_Asm_d2]
+                addDs [Buf_f_d] addEs [ssubst], simpset()) 1);
 by (safe_tac (claset() addSDs [BufAC_Asm_d3]));
 by (REPEAT(dtac Buf_f_d_req 1));
 by (fast_tac (claset() addEs [ssubst]) 1);
 qed_spec_mp "BufAC_Asm_cong";
 
 (*adm_non_BufAC_Asm,BufAC_Asm_cong*)
-val BufAC_Cmt_d_req = prove_goal thy 
+val BufAC_Cmt_d_req = prove_goal (the_context ())
 "!!X. [|f:BufEq; s:BufAC_Asm; (s, f\\<cdot>s):BufAC_Cmt|] ==> (a\\<leadsto>b\\<leadsto>s, f\\<cdot>(a\\<leadsto>b\\<leadsto>s)):BufAC_Cmt"
  (K [
-	rtac (BufAC_Cmt_unfold RS iffD2) 1,
-	strip_tac 1,
-	ftac Buf_f_d_req 1,
-	auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
+        rtac (BufAC_Cmt_unfold RS iffD2) 1,
+        strip_tac 1,
+        ftac Buf_f_d_req 1,
+        auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
 
 (*adm_BufAC_Asm*)
 Goal "antitonP BufAC_Asm";
@@ -99,16 +99,16 @@
 b y   safe_tac HOL_cs;
 b y   rtac BufAC_Asm_empty 1;
 b y  force_tac (claset() addSDs [fstream_prefix]
-		addDs [BufAC_Asm_d2] addIs [BufAC_Asm_d],simpset()) 1;
+                addDs [BufAC_Asm_d2] addIs [BufAC_Asm_d],simpset()) 1;
 b y  force_tac (claset() addSDs [fstream_prefix]
-		addDs [] addIs []
-		addDs [BufAC_Asm_d3] addSIs [BufAC_Asm_d_req],simpset()) 1;
+                addDs [] addIs []
+                addDs [BufAC_Asm_d3] addSIs [BufAC_Asm_d_req],simpset()) 1;
 qed "BufAC_Asm_antiton";
 
 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
 Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
-		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
-		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
+                \    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
+                \    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
 by (res_inst_tac [("x","%i. 2*i")] exI 1);
 by (rtac allI 1);
 by (induct_tac "i" 1);
@@ -137,12 +137,12 @@
 *)
 by (rotate_tac 2 1);
 by (dtac BufAC_Asm_prefix2 1);
-by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1, rotate_tac ~1 1,etac ssubst 1]); 
+by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1, rotate_tac ~1 1,etac ssubst 1]);
 by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1]);
-by (		subgoal_tac "f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya" 1);
+by (            subgoal_tac "f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya" 1);
 by ( atac 2);
-by (		rotate_tac ~1 1);
-by (		Asm_full_simp_tac 1);
+by (            rotate_tac ~1 1);
+by (            Asm_full_simp_tac 1);
 by (hyp_subst_tac 1);
 (*
  1. \\<And>i d xa ya t ff ffa.
@@ -272,6 +272,6 @@
 Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
 by (rtac triv_admI 1);
 by (Clarify_tac 1);
-by (eatac Buf_Eq_imp_AC_lemma 1 1); 
+by (eatac Buf_Eq_imp_AC_lemma 1 1);
       (* this is what we originally aimed to show, using admissibilty :-( *)
 qed "adm_BufAC'";
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOLCF/FOCUS/Buffer_adm.thy	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy	Tue Sep 06 21:51:17 2005 +0200
@@ -1,9 +1,14 @@
-(*  Title: 	HOLCF/FOCUS/Buffer_adm.thy
+(*  Title:      HOLCF/FOCUS/Buffer_adm.thy
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
-
-One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility
+    Author:     David von Oheimb, TU Muenchen
 *)
 
-Buffer_adm = Buffer + Stream_adm
+header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
 
+theory Buffer_adm
+imports Buffer Stream_adm
+begin
+
+end
+
+
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/FOCUS.ML
--- a/src/HOLCF/FOCUS/FOCUS.ML	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/FOCUS.ML	Tue Sep 06 21:51:17 2005 +0200
@@ -1,11 +1,11 @@
-(*  Title: 	HOLCF/FOCUS/FOCUS.ML
+(*  Title:      HOLCF/FOCUS/FOCUS.ML
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 *)
 
-val ex_eqI = prove_goal thy "? xx. x = xx" (K [Auto_tac]);
-val ex2_eqI = prove_goal thy "? xx yy. x = xx & y = yy" (K [Auto_tac]);
-val eq_UU_symf = prove_goal thy "(UU = f x) = (f x = UU)" (K [Auto_tac]);
+val ex_eqI = prove_goal (the_context ()) "? xx. x = xx" (K [Auto_tac]);
+val ex2_eqI = prove_goal (the_context ()) "? xx yy. x = xx & y = yy" (K [Auto_tac]);
+val eq_UU_symf = prove_goal (the_context ()) "(UU = f x) = (f x = UU)" (K [Auto_tac]);
 
 AddSIs [ex_eqI, ex2_eqI];
 Addsimps[eq_UU_symf];
@@ -14,6 +14,6 @@
 qed "fstream_exhaust_slen_eq";
 
 Addsimps[thm "slen_less_1_eq", fstream_exhaust_slen_eq,
-		   thm "slen_fscons_eq", thm "slen_fscons_less_eq"];
+                   thm "slen_fscons_eq", thm "slen_fscons_less_eq"];
 Addsimps[thm "Suc_ile_eq"];
 AddEs  [strictI];
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/FOCUS.thy
--- a/src/HOLCF/FOCUS/FOCUS.thy	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/FOCUS.thy	Tue Sep 06 21:51:17 2005 +0200
@@ -1,8 +1,12 @@
-(*  Title: 	HOLCF/FOCUS/FOCUS.thy
+(*  Title:      HOLCF/FOCUS/FOCUS.thy
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
-
-top level of FOCUS
+    Author:     David von Oheimb, TU Muenchen
 *)
 
-FOCUS = Fstream
+header {* Top level of FOCUS *}
+
+theory FOCUS
+imports Fstream
+begin
+
+end
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/Fstream.ML
--- a/src/HOLCF/FOCUS/Fstream.ML	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Fstream.ML	Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(*  Title: 	HOLCF/FOCUS/Fstream.ML
+(*  Title:      HOLCF/FOCUS/Fstream.ML
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 *)
 
 Addsimps[eq_UU_iff RS sym];
@@ -19,60 +19,60 @@
 by (Simp_tac 1);
 qed "fscons_def2";
 
-qed_goal "fstream_exhaust" thy "x = UU |  (? a y. x = a~> y)" (fn _ => [
-	simp_tac (simpset() addsimps [fscons_def2]) 1,
-	cut_facts_tac [thm "stream.exhaust"] 1,
-	fast_tac (claset() addDs [not_Undef_is_Def RS iffD1]) 1]);
+qed_goal "fstream_exhaust" (the_context ()) "x = UU |  (? a y. x = a~> y)" (fn _ => [
+        simp_tac (simpset() addsimps [fscons_def2]) 1,
+        cut_facts_tac [thm "stream.exhaust"] 1,
+        fast_tac (claset() addDs [not_Undef_is_Def RS iffD1]) 1]);
 
-qed_goal "fstream_cases" thy "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P" 
+qed_goal "fstream_cases" (the_context ()) "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P"
  (fn prems => [
-	cut_facts_tac [fstream_exhaust] 1,
-	etac disjE 1,
-	 eresolve_tac prems 1,
-	REPEAT(etac exE 1),
-	eresolve_tac prems 1]);
+        cut_facts_tac [fstream_exhaust] 1,
+        etac disjE 1,
+         eresolve_tac prems 1,
+        REPEAT(etac exE 1),
+        eresolve_tac prems 1]);
 
 fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i
-			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
+                          THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
 
-qed_goal "fstream_exhaust_eq" thy "(x ~= UU) = (? a y. x = a~> y)" (fn _ => [
-	simp_tac(simpset() addsimps [fscons_def2,thm "stream_exhaust_eq"]) 1,
-	fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
+qed_goal "fstream_exhaust_eq" (the_context ()) "(x ~= UU) = (? a y. x = a~> y)" (fn _ => [
+        simp_tac(simpset() addsimps [fscons_def2,thm "stream_exhaust_eq"]) 1,
+        fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
 
 
-qed_goal "fscons_not_empty" thy "a~> s ~= <>" (fn _ => [
-	stac fscons_def2 1,
+qed_goal "fscons_not_empty" (the_context ()) "a~> s ~= <>" (fn _ => [
+        stac fscons_def2 1,
         Simp_tac 1]);
 Addsimps[fscons_not_empty];
 
 
-qed_goal "fscons_inject" thy "(a~> s = b~> t) = (a = b &  s = t)" (fn _ => [
-	simp_tac (HOL_ss addsimps [fscons_def2]) 1,
-	stac (hd lift.inject RS sym) 1, (*2*back();*)
+qed_goal "fscons_inject" (the_context ()) "(a~> s = b~> t) = (a = b &  s = t)" (fn _ => [
+        simp_tac (HOL_ss addsimps [fscons_def2]) 1,
+        stac (hd lift.inject RS sym) 1, (*2*back();*)
         Simp_tac 1]);
 Addsimps[fscons_inject];
 
-qed_goal "fstream_prefix" thy "a~> s << t ==> ? tt. t = a~> tt &  s << tt" (fn prems =>[
-	cut_facts_tac prems 1,
-	res_inst_tac [("x","t")] (thm "stream.casedist") 1,
-	 cut_facts_tac [fscons_not_empty] 1,
-	 fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2]) 1,
-	asm_full_simp_tac (HOL_ss addsimps [fscons_def2]) 1,
-	dtac (thm "stream_flat_prefix") 1,
-	rtac Def_not_UU 1,
-	fast_tac HOL_cs 1]);
+qed_goal "fstream_prefix" (the_context ()) "a~> s << t ==> ? tt. t = a~> tt &  s << tt" (fn prems =>[
+        cut_facts_tac prems 1,
+        res_inst_tac [("x","t")] (thm "stream.casedist") 1,
+         cut_facts_tac [fscons_not_empty] 1,
+         fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2]) 1,
+        asm_full_simp_tac (HOL_ss addsimps [fscons_def2]) 1,
+        dtac (thm "stream_flat_prefix") 1,
+        rtac Def_not_UU 1,
+        fast_tac HOL_cs 1]);
 
-qed_goal "fstream_prefix'" thy
-	"x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))" (fn _ => [
-	simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "stream_prefix'"])1,
-	Step_tac 1,
-	 ALLGOALS(etac swap),
-	 fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2,
-	rtac Lift_cases 1,
-	 contr_tac 1,
-	Step_tac 1,
-	dtac (Def_inject_less_eq RS iffD1) 1,
-	Fast_tac 1]);
+qed_goal "fstream_prefix'" (the_context ())
+        "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))" (fn _ => [
+        simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "stream_prefix'"])1,
+        Step_tac 1,
+         ALLGOALS(etac swap),
+         fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2,
+        rtac Lift_cases 1,
+         contr_tac 1,
+        Step_tac 1,
+        dtac (Def_inject_less_eq RS iffD1) 1,
+        Fast_tac 1]);
 Addsimps[fstream_prefix'];
 
 (* ------------------------------------------------------------------------- *)
@@ -80,22 +80,22 @@
 section "ft & rt";
 
 bind_thm("ft_empty",hd (thms "stream.sel_rews"));
-qed_goalw "ft_fscons" thy [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [
-	(Simp_tac 1)]);
+qed_goalw "ft_fscons" (the_context ()) [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [
+        (Simp_tac 1)]);
 Addsimps[ft_fscons];
 
 bind_thm("rt_empty",hd (tl (thms "stream.sel_rews")));
-qed_goalw "rt_fscons" thy [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [
-	(Simp_tac 1)]);
+qed_goalw "rt_fscons" (the_context ()) [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [
+        (Simp_tac 1)]);
 Addsimps[rt_fscons];
 
-qed_goalw "ft_eq" thy [fscons_def] "(ft\\<cdot>s = Def a) = (? t. s = a~> t)" (K [
-	Simp_tac 1,
-	Safe_tac,
-	 etac subst 1,
-	 rtac exI 1,
-	 rtac (thm "surjectiv_scons" RS sym) 1,
-	Simp_tac 1]);
+qed_goalw "ft_eq" (the_context ()) [fscons_def] "(ft\\<cdot>s = Def a) = (? t. s = a~> t)" (K [
+        Simp_tac 1,
+        Safe_tac,
+         etac subst 1,
+         rtac exI 1,
+         rtac (thm "surjectiv_scons" RS sym) 1,
+        Simp_tac 1]);
 Addsimps[ft_eq];
 
 Goal "(d\\<leadsto>y = x) = (ft\\<cdot>x = Def d & rt\\<cdot>x = y)";
@@ -110,95 +110,95 @@
 
 section "take";
 
-qed_goalw "fstream_take_Suc" thy [fscons_def]
-	"stream_take (Suc n)\\<cdot>(a~> s) = a~> stream_take n\\<cdot>s" (K [
-	Simp_tac 1]);
+qed_goalw "fstream_take_Suc" (the_context ()) [fscons_def]
+        "stream_take (Suc n)\\<cdot>(a~> s) = a~> stream_take n\\<cdot>s" (K [
+        Simp_tac 1]);
 Addsimps[fstream_take_Suc];
 
 
 (* ------------------------------------------------------------------------- *)
 
 section "slen";
-	
+
 (*bind_thm("slen_empty", slen_empty);*)
 
-qed_goalw "slen_fscons" thy [fscons_def] "#(m~> s) = iSuc (#s)" (fn _ => [
-	(Simp_tac 1)]);
+qed_goalw "slen_fscons" (the_context ()) [fscons_def] "#(m~> s) = iSuc (#s)" (fn _ => [
+        (Simp_tac 1)]);
 
-qed_goal "slen_fscons_eq" thy 
-	"(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
-	simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq"]) 1,
-	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
+qed_goal "slen_fscons_eq" (the_context ())
+        "(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
+        simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq"]) 1,
+        fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
 
-qed_goal "slen_fscons_eq_rev" thy 
-	"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
-	simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq_rev"]) 1,
-	step_tac (HOL_cs addSEs [DefE]) 1,
-	step_tac (HOL_cs addSEs [DefE]) 1,
-	step_tac (HOL_cs addSEs [DefE]) 1,
-	step_tac (HOL_cs addSEs [DefE]) 1,
-	step_tac (HOL_cs addSEs [DefE]) 1,
-	step_tac (HOL_cs addSEs [DefE]) 1,
-	etac swap 1,
-	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
+qed_goal "slen_fscons_eq_rev" (the_context ())
+        "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
+        simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq_rev"]) 1,
+        step_tac (HOL_cs addSEs [DefE]) 1,
+        step_tac (HOL_cs addSEs [DefE]) 1,
+        step_tac (HOL_cs addSEs [DefE]) 1,
+        step_tac (HOL_cs addSEs [DefE]) 1,
+        step_tac (HOL_cs addSEs [DefE]) 1,
+        step_tac (HOL_cs addSEs [DefE]) 1,
+        etac swap 1,
+        fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
 
-qed_goal "slen_fscons_less_eq" thy 
-	"(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))" (fn _ => [
-	stac slen_fscons_eq_rev 1,
-	fast_tac (HOL_cs addSDs [fscons_inject RS iffD1]) 1]);
+qed_goal "slen_fscons_less_eq" (the_context ())
+        "(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))" (fn _ => [
+        stac slen_fscons_eq_rev 1,
+        fast_tac (HOL_cs addSDs [fscons_inject RS iffD1]) 1]);
 
 
 (* ------------------------------------------------------------------------- *)
 
 section "induction";
 
-qed_goal "fstream_ind" thy 
-	"[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" (fn prems => [
-	cut_facts_tac prems 1,
-	etac (thm "stream.ind") 1,
-	 atac 1,
-	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] 
-			 addEs (tl (tl prems) RL [fscons_def2 RS subst])) 1]);
+qed_goal "fstream_ind" (the_context ())
+        "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" (fn prems => [
+        cut_facts_tac prems 1,
+        etac (thm "stream.ind") 1,
+         atac 1,
+        fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]
+                         addEs (tl (tl prems) RL [fscons_def2 RS subst])) 1]);
 
-qed_goal "fstream_ind2" thy 
+qed_goal "fstream_ind2" (the_context ())
   "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" (fn prems => [
-	cut_facts_tac prems 1,
-	etac (thm "stream_ind2") 1,
-	  atac 1,
-	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] 
-			 addIs ([hd(tl(tl prems))]RL[fscons_def2 RS subst]))1,
-	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] 
-			 addEs [hd(tl(tl(tl prems))RL[fscons_def2 RS subst]
-						 RL[fscons_def2 RS subst])])1]);
+        cut_facts_tac prems 1,
+        etac (thm "stream_ind2") 1,
+          atac 1,
+        fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]
+                         addIs ([hd(tl(tl prems))]RL[fscons_def2 RS subst]))1,
+        fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]
+                         addEs [hd(tl(tl(tl prems))RL[fscons_def2 RS subst]
+                                                 RL[fscons_def2 RS subst])])1]);
 
 
 (* ------------------------------------------------------------------------- *)
 
 section "fsfilter";
 
-qed_goalw "fsfilter_empty" thy [fsfilter_def] "A(C)UU = UU" (fn _ => [
-	rtac (thm "sfilter_empty") 1]);
+qed_goalw "fsfilter_empty" (the_context ()) [fsfilter_def] "A(C)UU = UU" (fn _ => [
+        rtac (thm "sfilter_empty") 1]);
 
-qed_goalw "fsfilter_fscons" thy [fsfilter_def] 
-	"A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" (fn _ => [
-	simp_tac (simpset() addsimps [fscons_def2,thm "sfilter_scons",If_and_if]) 1]);
+qed_goalw "fsfilter_fscons" (the_context ()) [fsfilter_def]
+        "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" (fn _ => [
+        simp_tac (simpset() addsimps [fscons_def2,thm "sfilter_scons",If_and_if]) 1]);
 
-qed_goal "fsfilter_emptys" thy "{}(C)x = UU" (fn _ => [
-	res_inst_tac [("x","x")] fstream_ind 1,
-	  resolve_tac adm_lemmas 1,
-	   cont_tacR 1,
-	 rtac fsfilter_empty 1,
-	asm_simp_tac (simpset()addsimps [fsfilter_fscons]) 1]);
+qed_goal "fsfilter_emptys" (the_context ()) "{}(C)x = UU" (fn _ => [
+        res_inst_tac [("x","x")] fstream_ind 1,
+          resolve_tac adm_lemmas 1,
+           cont_tacR 1,
+         rtac fsfilter_empty 1,
+        asm_simp_tac (simpset()addsimps [fsfilter_fscons]) 1]);
 
-qed_goal "fsfilter_insert" thy "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" (fn _=> [
-	simp_tac (simpset() addsimps [thm "fsfilter_fscons"]) 1]);
+qed_goal "fsfilter_insert" (the_context ()) "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" (fn _=> [
+        simp_tac (simpset() addsimps [thm "fsfilter_fscons"]) 1]);
 
-qed_goal "fsfilter_single_in" thy "{a}(C)a~> x = a~> ({a}(C)x)" (fn _=> [
-	rtac fsfilter_insert 1]);
+qed_goal "fsfilter_single_in" (the_context ()) "{a}(C)a~> x = a~> ({a}(C)x)" (fn _=> [
+        rtac fsfilter_insert 1]);
 
-qed_goal "fsfilter_single_out" thy "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" (fn prems => [
-	cut_facts_tac prems 1,
-	asm_simp_tac (simpset() addsimps[fsfilter_fscons]) 1]);
+qed_goal "fsfilter_single_out" (the_context ()) "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" (fn prems => [
+        cut_facts_tac prems 1,
+        asm_simp_tac (simpset() addsimps[fsfilter_fscons]) 1]);
 
 Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> \\<exists>j t. Y j = a\\<leadsto>t";
 by (case_tac "max_in_chain i Y" 1);
@@ -235,5 +235,3 @@
 by  (atac 1);
 by (Asm_simp_tac 1);
 qed "fstream_lub_lemma";
-
-
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy	Tue Sep 06 21:51:17 2005 +0200
@@ -1,45 +1,49 @@
-(*  Title: 	HOLCF/FOCUS/Fstream.thy
+(*  Title:      HOLCF/FOCUS/Fstream.thy
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 
 FOCUS streams (with lifted elements)
 ###TODO: integrate Fstreams.thy
 *)
 
-(* FOCUS flat streams *)
-
-Fstream = Stream + 
+header {* FOCUS flat streams *}
 
-default type
+theory Fstream
+imports Stream
+begin
 
-types 'a fstream = ('a lift) stream
+defaultsort type
+
+types 'a fstream = "'a lift stream"
 
 consts
 
-  fscons	:: "'a     \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
-  fsfilter	:: "'a set \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
+  fscons        :: "'a     \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
+  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
 
 syntax
 
-  "@emptystream":: "'a fstream" 			("<>")
-  "@fscons"	:: "'a \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream"	("(_~>_)"    [66,65] 65)
-  "@fsfilter"	:: "'a set \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream"	("(_'(C')_)" [64,63] 63)
+  "@emptystream":: "'a fstream"                           ("<>")
+  "@fscons"     :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_~>_)"    [66,65] 65)
+  "@fsfilter"   :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_'(C')_)" [64,63] 63)
 
 syntax (xsymbols)
 
-  "@fscons"	:: "'a \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream"	("(_\\<leadsto>_)"
-								     [66,65] 65)
-  "@fsfilter"	:: "'a set \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_\\<copyright>_)"
-								     [64,63] 63)
+  "@fscons"     :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_\<leadsto>_)"
+                                                                     [66,65] 65)
+  "@fsfilter"   :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)"
+                                                                     [64,63] 63)
 translations
 
-  "<>"    => "\\<bottom>"
-  "a~>s"  == "fscons a\\<cdot>s"
-  "A(C)s" == "fsfilter A\\<cdot>s"
+  "<>"    => "\<bottom>"
+  "a~>s"  == "fscons a\<cdot>s"
+  "A(C)s" == "fsfilter A\<cdot>s"
 
 defs
 
-  fscons_def	"fscons a   \\<equiv> \\<Lambda> s. Def a && s"
-  fsfilter_def  "fsfilter A \\<equiv> sfilter\\<cdot>(flift2 (\\<lambda>x. x\\<in>A))"
+  fscons_def:    "fscons a   \<equiv> \<Lambda> s. Def a && s"
+  fsfilter_def:  "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/Stream_adm.ML
--- a/src/HOLCF/FOCUS/Stream_adm.ML	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.ML	Tue Sep 06 21:51:17 2005 +0200
@@ -1,6 +1,6 @@
-(*  Title: 	HOLCF/ex/Stream_adm.ML
+(*  Title:      HOLCF/ex/Stream_adm.ML
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 *)
 
 (* ----------------------------------------------------------------------- *)
@@ -77,66 +77,66 @@
 by ( etac (thm "slen_rt_mult") 1);
 by (dtac mp 1);
 by (etac (thm "monofun_rt_mult") 1);
-by (mp_tac 1); 
+by (mp_tac 1);
 by (atac 1);
 qed "stream_monoP2I";
 
 Goal "[| !i. ? l. !x y. \
 \Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;\
 \   down_cont F |] ==> adm (%x. x:gfp F)";
-byev[	etac (INTER_down_iterate_is_gfp RS ssubst) 1, (* cont *)
-	Simp_tac 1,
-	resolve_tac adm_lemmas 1,
-	rtac flatstream_admI 1,
-	etac allE 1,
-	etac exE 1,
-	etac allE 1 THEN etac exE 1,
-	etac allE 1 THEN etac allE 1 THEN dtac mp 1, (* stream_monoP *)
-	 dtac (thm "ileI1") 1,
-	 dtac (thm "ile_trans") 1,
-	  rtac (thm "ile_iSuc") 1,
-	 dtac (thm "iSuc_ile_mono" RS iffD1) 1,
-	 atac 1,
-	dtac mp 1,
-	 etac is_ub_thelub 1,
-	Fast_tac 1];
+byev[   etac (INTER_down_iterate_is_gfp RS ssubst) 1, (* cont *)
+        Simp_tac 1,
+        resolve_tac adm_lemmas 1,
+        rtac flatstream_admI 1,
+        etac allE 1,
+        etac exE 1,
+        etac allE 1 THEN etac exE 1,
+        etac allE 1 THEN etac allE 1 THEN dtac mp 1, (* stream_monoP *)
+         dtac (thm "ileI1") 1,
+         dtac (thm "ile_trans") 1,
+          rtac (thm "ile_iSuc") 1,
+         dtac (thm "iSuc_ile_mono" RS iffD1) 1,
+         atac 1,
+        dtac mp 1,
+         etac is_ub_thelub 1,
+        Fast_tac 1];
 qed "stream_monoP2_gfp_admI";
 
 bind_thm("fstream_gfp_admI",stream_monoP2I RS stream_monoP2_gfp_admI);
 
-qed_goalw "stream_antiP2I" thy [stream_antiP_def]
+qed_goalw "stream_antiP2I" (the_context ()) [stream_antiP_def]
 "!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]\
 \ ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i" (K [
-	rtac allI 1,
-	induct_tac "i" 1,
-	 Simp_tac 1,
-	Simp_tac 1,
-	strip_tac 1,
-	etac allE 1 THEN etac all_dupE 1 THEN etac exE 1 THEN etac exE 1,
-	etac conjE 1,
-	case_tac "#x < Fin i" 1,
-	 fast_tac HOL_cs 1,
-	fold_goals_tac [thm "ile_def"],
-	mp_tac 1,
-	etac all_dupE 1 THEN dtac mp 1 THEN rtac refl_less 1,
-	etac ssubst 1,
+        rtac allI 1,
+        induct_tac "i" 1,
+         Simp_tac 1,
+        Simp_tac 1,
+        strip_tac 1,
+        etac allE 1 THEN etac all_dupE 1 THEN etac exE 1 THEN etac exE 1,
+        etac conjE 1,
+        case_tac "#x < Fin i" 1,
+         fast_tac HOL_cs 1,
+        fold_goals_tac [thm "ile_def"],
+        mp_tac 1,
+        etac all_dupE 1 THEN dtac mp 1 THEN rtac refl_less 1,
+        etac ssubst 1,
         etac allE 1 THEN mp_tac 1,
-	dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1,
-	etac conjE 1 THEN rtac conjI 1,
-	 etac (thm "slen_take_lemma3" RS ssubst) 1 THEN atac 1,
-	 atac 1,
-	etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac (thm "monofun_rt_mult") 1,
-	mp_tac 1,
-	atac 1]);
+        dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1,
+        etac conjE 1 THEN rtac conjI 1,
+         etac (thm "slen_take_lemma3" RS ssubst) 1 THEN atac 1,
+         atac 1,
+        etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac (thm "monofun_rt_mult") 1,
+        mp_tac 1,
+        atac 1]);
 
-qed_goalw "stream_antiP2_non_gfp_admI" thy [adm_def]
+qed_goalw "stream_antiP2_non_gfp_admI" (the_context ()) [adm_def]
 "!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] \
 \ ==> adm (%u. ~ u:gfp F)" (K [
-	asm_simp_tac (simpset() addsimps [INTER_down_iterate_is_gfp]) 1,
-	fast_tac (claset() addSDs [is_ub_thelub]) 1]);
+        asm_simp_tac (simpset() addsimps [INTER_down_iterate_is_gfp]) 1,
+        fast_tac (claset() addSDs [is_ub_thelub]) 1]);
 
-bind_thm ("fstream_non_gfp_admI", stream_antiP2I RS 
-				stream_antiP2_non_gfp_admI);
+bind_thm ("fstream_non_gfp_admI", stream_antiP2I RS
+                                stream_antiP2_non_gfp_admI);
 
 
 
@@ -165,7 +165,7 @@
 by (Fast_tac 1);
 qed "def_gfp_adm_nonP";
 
-Goalw [adm_def] 
+Goalw [adm_def]
 "{lub (range Y) |Y. chain Y & (\\<forall>i. Y i \\<in> P)} \\<subseteq> P \\<Longrightarrow> adm (\\<lambda>x. x\\<in>P)";
 by (Fast_tac 1);
 qed "adm_set";
diff -r 5c613b64bf0a -r ecf182ccc3ca src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Tue Sep 06 21:51:17 2005 +0200
@@ -1,28 +1,29 @@
-(*  Title: 	HOLCF/ex/Stream_adm.thy
+(*  Title:      HOLCF/ex/Stream_adm.thy
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
-
-Admissibility for streams
+    Author:     David von Oheimb, TU Muenchen
 *)
 
-Stream_adm = Stream + Continuity +
-
-consts
-
-  stream_monoP,
-  stream_antiP	:: "(('a stream) set \\<Rightarrow> ('a stream) set) \\<Rightarrow> bool"
+header {* Admissibility for streams *}
 
-defs
-
-  stream_monoP_def "stream_monoP F \\<equiv> \\<exists>Q i. \\<forall>P s. Fin i \\<le> #s \\<longrightarrow> 
-			(s \\<in> F P) = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
-  stream_antiP_def "stream_antiP F \\<equiv> \\<forall>P x. \\<exists>Q i. 
-		(#x  < Fin i \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> y \\<in> F P \\<longrightarrow> x \\<in> F P)) \\<and>
-		(Fin i <= #x \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> 
-		(y \\<in> F P) = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
+theory Stream_adm
+imports Stream Continuity
+begin
 
 constdefs
+
+  stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
+  "stream_monoP F \<equiv> \<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
+                    (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i rt s \<in> P)"
+
+  stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
+  "stream_antiP F \<equiv> \<forall>P x. \<exists>Q i.
+                (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
+                (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
+                (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i rt y \<in> P)))"
+
   antitonP :: "'a set => bool"
- "antitonP P \\<equiv> \\<forall>x y. x \\<sqsubseteq> y \\<longrightarrow> y\\<in>P \\<longrightarrow> x\\<in>P"
-  
+  "antitonP P \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end