# HG changeset patch
# User wenzelm
# Date 1149270097 -7200
# Node ID ec18656a2c102c07b9e478d3139512dab3b16c49
# Parent  957bcf55c98f2962c029aec75c1d8ee31b5303b0
tuned;

diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/FOCUS/Buffer.thy
--- a/src/HOLCF/FOCUS/Buffer.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -41,48 +41,50 @@
   SPSF11        = "State \<Rightarrow> SPF11"
   SPECS11       = "SPSF11 set"
 
-consts
+definition
 
   BufEq_F       :: "SPEC11 \<Rightarrow> SPEC11"
+  "BufEq_F B = {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         :: "SPEC11"
+  "BufEq = gfp BufEq_F"
+
   BufEq_alt     :: "SPEC11"
+  "BufEq_alt = 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   :: " (M fstream set) \<Rightarrow> (M fstream set)"
+  "BufAC_Asm_F A = {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     :: " (M fstream set)"
+  "BufAC_Asm = gfp BufAC_Asm_F"
+
   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"
-
-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"
-
-  BufAC_Cmt_F_def: "BufAC_Cmt_F C \<equiv> {(s,t). \<forall>d x.
+  "BufAC_Cmt_F C = {(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     :: "((M fstream * D fstream) set)"
+  "BufAC_Cmt = gfp BufAC_Cmt_F"
 
-  BufSt_F_def:   "BufSt_F H \<equiv> {h. \<forall>s  . h s      \<cdot><>        = <>         \<and>
+  BufAC         :: "SPEC11"
+  "BufAC = {f. \<forall>x. x\<in>BufAC_Asm \<longrightarrow> (x,f\<cdot>x)\<in>BufAC_Cmt}"
+
+  BufSt_F       :: "SPECS11 \<Rightarrow> SPECS11"
+  "BufSt_F H = {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_P       :: "SPECS11"
+  "BufSt_P = gfp BufSt_F"
 
-ML {* use_legacy_bindings (the_context ()) *}
+  BufSt         :: "SPEC11"
+  "BufSt = {f. \<exists>h\<in>BufSt_P. f = h \<currency>}"
+
 
 lemma set_cong: "!!X. A = B ==> (x:A) = (x:B)"
 by (erule subst, rule refl)
@@ -100,7 +102,7 @@
 lemma mono_BufEq_F: "mono BufEq_F"
 by (unfold mono_def BufEq_F_def, fast)
 
-lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN def_gfp_unfold]];
+lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN eq_reflection, THEN def_gfp_unfold]]
 
 lemma BufEq_unfold: "(f:BufEq) = (!d. f\<cdot>(Md d\<leadsto><>) = <> &
                  (!x. ? ff:BufEq. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>(ff\<cdot>x)))"
@@ -125,7 +127,8 @@
 lemma mono_BufAC_Asm_F: "mono BufAC_Asm_F"
 by (unfold mono_def BufAC_Asm_F_def, fast)
 
-lemmas BufAC_Asm_fix = mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN def_gfp_unfold]]
+lemmas BufAC_Asm_fix =
+  mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN eq_reflection, THEN def_gfp_unfold]]
 
 lemma BufAC_Asm_unfold: "(s:BufAC_Asm) = (s = <> | (? d x. 
         s = Md d\<leadsto>x & (x = <> | (ft\<cdot>x = Def \<bullet> & (rt\<cdot>x):BufAC_Asm))))"
@@ -150,7 +153,8 @@
 lemma mono_BufAC_Cmt_F: "mono BufAC_Cmt_F"
 by (unfold mono_def BufAC_Cmt_F_def, fast)
 
-lemmas BufAC_Cmt_fix = mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN def_gfp_unfold]]
+lemmas BufAC_Cmt_fix =
+  mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN eq_reflection, THEN def_gfp_unfold]]
 
 lemma BufAC_Cmt_unfold: "((s,t):BufAC_Cmt) = (!d x. 
      (s = <>       -->      t = <>) & 
@@ -225,7 +229,8 @@
 lemma mono_BufSt_F: "mono BufSt_F"
 by (unfold mono_def BufSt_F_def, fast)
 
-lemmas BufSt_P_fix = mono_BufSt_F [THEN BufSt_P_def [THEN def_gfp_unfold]]
+lemmas BufSt_P_fix =
+  mono_BufSt_F [THEN BufSt_P_def [THEN eq_reflection, THEN def_gfp_unfold]]
 
 lemma BufSt_P_unfold: "(h:BufSt_P) = (!s. h s\<cdot><> = <> & 
            (!d x. h \<currency>     \<cdot>(Md d\<leadsto>x)   =    h (Sd d)\<cdot>x & 
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOLCF/FOCUS/Buffer_adm.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -235,7 +235,7 @@
 
 lemma adm_BufAC_Asm: "adm (\<lambda>x. x\<in>BufAC_Asm)"
 apply (rule def_gfp_admI)
-apply (rule BufAC_Asm_def)
+apply (rule BufAC_Asm_def [THEN eq_reflection])
 apply (safe)
 apply (unfold BufAC_Asm_F_def)
 apply (safe)
@@ -269,7 +269,7 @@
 
 lemma adm_non_BufAC_Asm': "adm (\<lambda>u. u \<notin> BufAC_Asm)" (* uses antitonP *)
 apply (rule def_gfp_adm_nonP)
-apply (rule BufAC_Asm_def)
+apply (rule BufAC_Asm_def [THEN eq_reflection])
 apply (unfold BufAC_Asm_F_def)
 apply (safe)
 apply (erule contrapos_np)
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -16,35 +16,27 @@
 
 types 'a fstream = "'a lift stream"
 
-consts
-
+definition
   fscons        :: "'a     \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
-  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
+  "fscons a = (\<Lambda> s. Def a && s)"
 
-syntax
+  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
+  "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))"
 
-  "@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)
+abbreviation
+  emptystream   :: "'a fstream"                          ("<>")
+  "<> == \<bottom>"
 
-  "@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
+  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_~>_)"    [66,65] 65)
+  "a~>s == fscons a\<cdot>s"
 
-  "<>"    => "\<bottom>"
-  "a~>s"  == "fscons a\<cdot>s"
-  "A(C)s" == "fsfilter A\<cdot>s"
+  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_'(C')_)" [64,63] 63)
+  "A(C)s == fsfilter A\<cdot>s"
 
-defs
+const_syntax (xsymbols)
+  fscons'  ("(_\<leadsto>_)"                                                 [66,65] 65)
+  fsfilter'  ("(_\<copyright>_)"                                               [64,63] 63)
 
-  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 ()) *}
 
 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
 apply (rule flat_eq [THEN iffD1, symmetric])
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -12,44 +12,35 @@
 
 types 'a fstream = "('a lift) stream"
 
-consts
-
+definition
   fsingleton    :: "'a => 'a fstream"  ("<_>" [1000] 999)
+  fsingleton_def2: "fsingleton = (%a. Def a && UU)"
+
   fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
+  "fsfilter A = sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
+
   fsmap		:: "('a => 'b) => 'a fstream -> 'b fstream"
+  "fsmap f = smap$(flift2 f)"
 
   jth           :: "nat => 'a fstream => 'a"
+  "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary)"
 
   first         :: "'a fstream => 'a"
+  "first = (%s. jth 0 s)"
+
   last          :: "'a fstream => 'a"
+  "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary)
+              | Infty => arbitrary)"
 
 
-syntax
-
-  "@emptystream":: "'a fstream" 			("<>")
-  "@fsfilter"	:: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"	("(_'(C')_)" [64,63] 63)
-
-syntax (xsymbols)
-
-  "@fsfilter"	:: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)"
-								     [64,63] 63)
-translations
+abbreviation
+  emptystream :: "'a fstream" 			("<>")
+  "<> == \<bottom>"
+  fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"	("(_'(C')_)" [64,63] 63)
+  "A(C)s == fsfilter A\<cdot>s"
 
-  "<>"    => "\<bottom>"
-  "A(C)s" == "fsfilter A\<cdot>s"
-
-defs
-
-  fsingleton_def2:    "fsingleton  == %a. Def a && UU"
-
-  jth_def:            "jth == %n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary" 
-
-  first_def:          "first == %s. jth 0 s"
-  last_def:           "last == %s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary)
-                              | Infty => arbitrary"
-
-  fsfilter_def:       "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
-  fsmap_def:   	      "fsmap f  == smap$(flift2 f)"
+const_syntax (xsymbols)
+  fsfilter'  ("(_\<copyright>_)" [64,63] 63)
 
 
 lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -9,22 +9,21 @@
 imports Stream Continuity
 begin
 
-constdefs
+definition
 
   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\<cdot>rt\<cdot>s \<in> P)"
+  "stream_monoP F = (\<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\<cdot>rt\<cdot>s \<in> P))"
 
   stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
-  "stream_antiP F \<equiv> \<forall>P x. \<exists>Q i.
+  "stream_antiP F = (\<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\<cdot>rt\<cdot>y \<in> P)))"
+                (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>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 = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)"
 
-ML {* use_legacy_bindings (the_context ()) *}
 
 (* ----------------------------------------------------------------------- *)
 
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/ex/Dagstuhl.thy
--- a/src/HOLCF/ex/Dagstuhl.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Dagstuhl.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -7,16 +7,16 @@
 consts
   y  :: "'a"
 
-constdefs
+definition
   YS :: "'a stream"
-  "YS == fix$(LAM x. y && x)"
+  "YS = fix$(LAM x. y && x)"
   YYS :: "'a stream"
-  "YYS == fix$(LAM z. y && y && z)"
+  "YYS = fix$(LAM z. y && y && z)"
 
 lemma YS_def2: "YS = y && YS"
   apply (rule trans)
   apply (rule fix_eq2)
-  apply (rule YS_def)
+  apply (rule YS_def [THEN eq_reflection])
   apply (rule beta_cfun)
   apply simp
   done
@@ -24,14 +24,14 @@
 lemma YYS_def2: "YYS = y && y && YYS"
   apply (rule trans)
   apply (rule fix_eq2)
-  apply (rule YYS_def)
+  apply (rule YYS_def [THEN eq_reflection])
   apply (rule beta_cfun)
   apply simp
   done
 
 
 lemma lemma3: "YYS << y && YYS"
-  apply (rule YYS_def [THEN def_fix_ind])
+  apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind])
   apply simp_all
   apply (rule monofun_cfun_arg)
   apply (rule monofun_cfun_arg)
@@ -77,7 +77,7 @@
   done
 
 lemma lemma7: "YS << YYS"
-  apply (rule YS_def [THEN def_fix_ind])
+  apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind])
   apply simp_all
   apply (subst lemma5 [symmetric])
   apply (erule monofun_cfun_arg)
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Dnat.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -9,9 +9,9 @@
 
 domain dnat = dzero | dsucc (dpred :: dnat)
 
-constdefs
+definition
   iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
-  "iterator == fix $ (LAM h n f x.
+  "iterator = fix $ (LAM h n f x.
     case n of dzero => x
       | dsucc $ m => f $ (h $ m $ f $ x))"
 
@@ -20,7 +20,7 @@
 *}
 
 ML_setup {*
-bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def")
+bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def" RS eq_reflection)
         "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))");
 *}
 
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/ex/Focus_ex.thy
--- a/src/HOLCF/ex/Focus_ex.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -108,33 +108,23 @@
 arities tc:: (pcpo, pcpo) pcpo
 
 consts
+  Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
 
-is_f     ::
- "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
-is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
-            'b stream => 'c stream => bool"
-is_g     :: "('b stream -> 'c stream) => bool"
-def_g    :: "('b stream -> 'c stream) => bool"
-Rf       ::
-"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
+definition
+  is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
+  "is_f f = (!i1 i2 o1 o2. f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
 
-defs
-
-is_f:           "is_f f == (!i1 i2 o1 o2.
-                        f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
-
-is_net_g:       "is_net_g f x y == (? z.
+  is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
+    'b stream => 'c stream => bool"
+  "is_net_g f x y == (? z.
                         <y,z> = f$<x,z> &
                         (!oy hz. <oy,hz> = f$<x,hz> --> z << hz))"
 
-is_g:           "is_g g  == (? f.
-                        is_f f  &
-                        (!x y. g$x = y --> is_net_g f x y))"
+  is_g :: "('b stream -> 'c stream) => bool"
+  "is_g g  == (? f. is_f f  & (!x y. g$x = y --> is_net_g f x y))"
 
-
-def_g:          "def_g g == (? f.
-                        is_f f  &
-                        g = (LAM x. cfst$(f$<x,fix$(LAM  k. csnd$(f$<x,k>))>)))"
+  def_g :: "('b stream -> 'c stream) => bool"
+  "def_g g == (? f. is_f f  & g = (LAM x. cfst$(f$<x,fix$(LAM  k. csnd$(f$<x,k>))>)))"
 
 
 (* first some logical trading *)
@@ -143,7 +133,7 @@
 "is_g(g) =
   (? f. is_f(f) &  (!x.(? z. <g$x,z> = f$<x,z> &
                    (! w y. <y,w> = f$<x,w>  --> z << w))))"
-apply (simp add: is_g is_net_g)
+apply (simp add: is_g_def is_net_g_def)
 apply fast
 done
 
@@ -191,7 +181,7 @@
 done
 
 lemma lemma3: "def_g(g) --> is_g(g)"
-apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g", thm "lemma1", thm "lemma2"]) 1 *})
+apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g_def", thm "lemma1", thm "lemma2"]) 1 *})
 apply (rule impI)
 apply (erule exE)
 apply (rule_tac x = "f" in exI)
@@ -218,7 +208,7 @@
 
 lemma lemma4: "is_g(g) --> def_g(g)"
 apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
-  addsimps [thm "lemma1", thm "lemma2", thm "def_g"]) 1 *})
+  addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
 apply (rule impI)
 apply (erule exE)
 apply (rule_tac x = "f" in exI)
@@ -262,7 +252,7 @@
   is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
   -->
   (? g. def_g(g::'b stream -> 'c stream ))"
-apply (simp add: def_g)
+apply (simp add: def_g_def)
 done
 
 theorem conservative_loopback:
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Hoare.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -28,15 +28,13 @@
   b1 :: "'a -> tr"
   b2 :: "'a -> tr"
   g :: "'a -> 'a"
-  p :: "'a -> 'a"
-  q :: "'a -> 'a"
 
-defs
-  p_def:  "p == fix$(LAM f. LAM x.
-                 If b1$x then f$(g$x) else x fi)"
+definition
+  p :: "'a -> 'a"
+  "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)"
 
-  q_def:  "q == fix$(LAM f. LAM x.
-                 If b1$x orelse b2$x then f$(g$x) else x fi)"
+  q :: "'a -> 'a"
+  "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)"
 
 
 (* --------- pure HOLCF logic, some little lemmas ------ *)
@@ -106,13 +104,13 @@
 
 lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi"
 apply (rule trans)
-apply (rule p_def [THEN fix_eq3])
+apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
 apply simp
 done
 
 lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"
 apply (rule trans)
-apply (rule q_def [THEN fix_eq3])
+apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
 apply simp
 done
 
@@ -233,7 +231,7 @@
 (* -------- results about p for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
 
 lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
-apply (rule p_def [THEN def_fix_ind])
+apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
 apply (rule adm_all)
 apply (rule allI)
 apply (rule adm_eq)
@@ -258,7 +256,7 @@
 (* -------- results about q for case  (ALL k. b1$(iterate k$g$x)=TT) ------- *)
 
 lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
-apply (rule q_def [THEN def_fix_ind])
+apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
 apply (rule adm_all)
 apply (rule allI)
 apply (rule adm_eq)
@@ -288,7 +286,7 @@
 done
 
 lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
-apply (rule q_def [THEN def_fix_ind])
+apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
 apply (rule adm_all)
 apply (rule allI)
 apply (rule adm_eq)
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Loop.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -9,13 +9,12 @@
 imports HOLCF
 begin
 
-constdefs
+definition
   step  :: "('a -> tr)->('a -> 'a)->'a->'a"
-  "step == (LAM b g x. If b$x then g$x else x fi)"
+  "step = (LAM b g x. If b$x then g$x else x fi)"
 
   while :: "('a -> tr)->('a -> 'a)->'a->'a"
-  "while == (LAM b g. fix$(LAM f x.
-    If b$x then f$(g$x) else x fi))"
+  "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))"
 
 (* ------------------------------------------------------------------------- *)
 (* access to definitions                                                     *)
diff -r 957bcf55c98f -r ec18656a2c10 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Stream.thy	Fri Jun 02 19:41:37 2006 +0200
@@ -11,47 +11,45 @@
 
 domain 'a stream = "&&" (ft::'a) (lazy rt::"'a stream") (infixr 65)
 
-consts
-
+definition
   smap          :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream"
-  sfilter       :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream"
-  slen          :: "'a stream \<Rightarrow> inat"                   ("#_" [1000] 1000)
+  "smap = fix\<cdot>(\<Lambda> h f s. case s of x && xs \<Rightarrow> f\<cdot>x && h\<cdot>f\<cdot>xs)"
 
-defs
+  sfilter       :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream"
+  "sfilter = fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
+                                     If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
 
-  smap_def:     "smap    \<equiv> fix\<cdot>(\<Lambda> h f s. case s of x && xs \<Rightarrow> f\<cdot>x && h\<cdot>f\<cdot>xs)"
-  sfilter_def:  "sfilter \<equiv> fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
-                                     If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
-  slen_def:     "#s \<equiv> if stream_finite s
-                      then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>"
+  slen          :: "'a stream \<Rightarrow> inat"                   ("#_" [1000] 1000)
+  "#s = (if stream_finite s then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
+
 
 (* concatenation *)
 
-consts
+definition
+  i_rt :: "nat => 'a stream => 'a stream" (* chops the first i elements *)
+  "i_rt = (%i s. iterate i$rt$s)"
 
-  i_rt :: "nat => 'a stream => 'a stream" (* chops the first i elements *)
   i_th :: "nat => 'a stream => 'a"        (* the i-th element *)
+  "i_th = (%i s. ft$(i_rt i s))"
 
   sconc         :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65)
-  constr_sconc  :: "'a stream => 'a stream => 'a stream" (* constructive *)
-  constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
-
-defs
-  i_rt_def: "i_rt == %i s. iterate i$rt$s"
-  i_th_def: "i_th == %i s. ft$(i_rt i s)"
+  "s1 ooo s2 = (case #s1 of
+                  Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
+               | \<infinity>     \<Rightarrow> s1)"
 
-  sconc_def: "s1 ooo s2 == case #s1 of
-                       Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
-                     | \<infinity>     \<Rightarrow> s1"
-
-  constr_sconc_def: "constr_sconc s1 s2 == case #s1 of
-                                             Fin n \<Rightarrow> constr_sconc' n s1 s2
-                                           | \<infinity>    \<Rightarrow> s1"
+consts
+  constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
 primrec
   constr_sconc'_0:   "constr_sconc' 0 s1 s2 = s2"
   constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 &&
                                                     constr_sconc' n (rt$s1) s2"
 
+definition
+  constr_sconc  :: "'a stream => 'a stream => 'a stream" (* constructive *)
+  "constr_sconc s1 s2 = (case #s1 of
+                          Fin n \<Rightarrow> constr_sconc' n s1 s2
+                        | \<infinity>    \<Rightarrow> s1)"
+
 
 declare stream.rews [simp add]
 
@@ -519,7 +517,7 @@
 section "smap"
 
 lemma smap_unfold: "smap = (\<Lambda> f t. case t of x&&xs \<Rightarrow> f$x && smap$f$xs)"
-by (insert smap_def [THEN fix_eq2], auto)
+by (insert smap_def [THEN eq_reflection, THEN fix_eq2], auto)
 
 lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (subst smap_unfold, simp)
@@ -538,7 +536,7 @@
 lemma sfilter_unfold:
  "sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
   If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
-by (insert sfilter_def [THEN fix_eq2], auto)
+by (insert sfilter_def [THEN eq_reflection, THEN fix_eq2], auto)
 
 lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
 apply (rule ext_cfun)