# HG changeset patch
# User wenzelm
# Date 1192969308 -7200
# Node ID 2c8caac48adeb57f76400617a51174b5f1bf90d8
# Parent  d91391a8705b9b543ffe70421edf42a4782a2a05
modernized specifications ('definition', 'abbreviation', 'notation');

diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Adm.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -13,12 +13,13 @@
 
 subsection {* Definitions *}
 
-constdefs
-  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
-  "adm P \<equiv> \<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i)"
+definition
+  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
+  "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
 
-  compact :: "'a::cpo \<Rightarrow> bool"
-  "compact k \<equiv> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
+definition
+  compact :: "'a::cpo \<Rightarrow> bool" where
+  "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
 
 lemma admI:
    "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Cfun.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -28,14 +28,14 @@
 syntax (xsymbols)
   "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
 
-syntax
-  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_$/_)" [999,1000] 999)
+notation
+  Rep_CFun  ("(_$/_)" [999,1000] 999)
 
-syntax (xsymbols)
-  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>/_)" [999,1000] 999)
+notation (xsymbols)
+  Rep_CFun  ("(_\<cdot>/_)" [999,1000] 999)
 
-syntax (HTML output)
-  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>/_)" [999,1000] 999)
+notation (HTML output)
+  Rep_CFun  ("(_\<cdot>/_)" [999,1000] 999)
 
 subsection {* Syntax for continuous lambda abstraction *}
 
@@ -43,7 +43,7 @@
 
 parse_translation {*
 (* rewrites (_cabs x t) => (Abs_CFun (%x. t)) *)
-  [mk_binder_tr ("_cabs", "Abs_CFun")];
+  [mk_binder_tr ("_cabs", @{const_syntax Abs_CFun})];
 *}
 
 text {* To avoid eta-contraction of body: *}
@@ -59,7 +59,7 @@
           val (x,t') = atomic_abs_tr' abs';
         in Syntax.const "_cabs" $ x $ t' end;
 
-  in [("Abs_CFun", cabs_tr')] end;
+  in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
 *}
 
 text {* Syntax for nested abstractions *}
@@ -95,7 +95,7 @@
 
 text {* Dummy patterns for continuous abstraction *}
 translations
-  "\<Lambda> _. t" => "Abs_CFun (\<lambda> _. t)"
+  "\<Lambda> _. t" => "CONST Abs_CFun (\<lambda> _. t)"
 
 
 subsection {* Continuous function space is pointed *}
@@ -439,9 +439,9 @@
   ID      :: "'a \<rightarrow> 'a"
   cfcomp  :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"
 
-syntax  "@oo" :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100)
-     
-translations  "f oo g" == "cfcomp\<cdot>f\<cdot>g"
+abbreviation
+  cfcomp_syn :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c"  (infixr "oo" 100)  where
+  "f oo g == cfcomp\<cdot>f\<cdot>g"
 
 defs
   ID_def: "ID \<equiv> (\<Lambda> x. x)"
@@ -481,9 +481,9 @@
 
 defaultsort pcpo
 
-constdefs
-  strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b"
-  "strictify \<equiv> (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+definition
+  strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
+  "strictify = (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
 
 text {* results about strictify *}
 
@@ -526,15 +526,15 @@
 
 subsection {* Continuous let-bindings *}
 
-constdefs
-  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
-  "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
+definition
+  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b" where
+  "CLet = (\<Lambda> s f. f\<cdot>s)"
 
 syntax
   "_CLet" :: "[letbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
 
 translations
   "_CLet (_binds b bs) e" == "_CLet b (_CLet bs e)"
-  "Let x = a in e" == "CLet\<cdot>a\<cdot>(\<Lambda> x. e)"
+  "Let x = a in e" == "CONST CLet\<cdot>a\<cdot>(\<Lambda> x. e)"
 
 end
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Cont.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -20,15 +20,17 @@
 
 subsection {* Definitions *}
 
-constdefs
-  monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"
-  "monofun f \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
+definition
+  monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
+  "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
 
-  contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def"
-  "contlub f \<equiv> \<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
+definition
+  contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def" where
+  "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
 
-  cont    :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "secnd cont. def"
-  "cont f    \<equiv> \<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
+definition
+  cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "secnd cont. def" where
+  "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
 
 lemma contlubI:
   "\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub f"
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Cprod.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -29,12 +29,12 @@
 instance unit :: pcpo
 by intro_classes simp
 
-constdefs
-  unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a"
-  "unit_when \<equiv> \<Lambda> a _. a"
+definition
+  unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
+  "unit_when = (\<Lambda> a _. a)"
 
 translations
-  "\<Lambda>(). t" == "unit_when\<cdot>t"
+  "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
 
 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
 by (simp add: unit_when_def)
@@ -192,18 +192,21 @@
 
 subsection {* Continuous versions of constants *}
 
-constdefs
-  cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *)
-  "cpair \<equiv> (\<Lambda> x y. (x, y))"
+definition
+  cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)"  -- {* continuous pairing *}  where
+  "cpair = (\<Lambda> x y. (x, y))"
+
+definition
+  cfst :: "('a * 'b) \<rightarrow> 'a" where
+  "cfst = (\<Lambda> p. fst p)"
 
-  cfst :: "('a * 'b) \<rightarrow> 'a"
-  "cfst \<equiv> (\<Lambda> p. fst p)"
+definition
+  csnd :: "('a * 'b) \<rightarrow> 'b" where
+  "csnd = (\<Lambda> p. snd p)"      
 
-  csnd :: "('a * 'b) \<rightarrow> 'b"
-  "csnd \<equiv> (\<Lambda> p. snd p)"      
-
-  csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c"
-  "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
+definition
+  csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
+  "csplit = (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
 
 syntax
   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
@@ -213,10 +216,10 @@
 
 translations
   "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
-  "\<langle>x, y\<rangle>"    == "cpair\<cdot>x\<cdot>y"
+  "\<langle>x, y\<rangle>"    == "CONST cpair\<cdot>x\<cdot>y"
 
 translations
-  "\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)"
+  "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
 
 
 subsection {* Convert all lemmas to the continuous versions *}
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Discrete.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -56,9 +56,9 @@
 
 subsection {* @{term undiscr} *}
 
-constdefs
-   undiscr :: "('a::type)discr => 'a"
-  "undiscr x == (case x of Discr y => y)"
+definition
+  undiscr :: "('a::type)discr => 'a" where
+  "undiscr x = (case x of Discr y => y)"
 
 lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
 by (simp add: undiscr_def)
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Fix.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -49,9 +49,9 @@
 
 subsection {* Least fixed point operator *}
 
-constdefs
-  "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a"
-  "fix \<equiv> \<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>"
+definition
+  "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where
+  "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
 
 text {* Binder syntax for @{term fix} *}
 
@@ -62,7 +62,7 @@
   "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10)
 
 translations
-  "\<mu> x. t" == "fix\<cdot>(\<Lambda> x. t)"
+  "\<mu> x. t" == "CONST fix\<cdot>(\<Lambda> x. t)"
 
 text {* Properties of @{term fix} *}
 
@@ -164,9 +164,9 @@
 
 subsection {* Recursive let bindings *}
 
-constdefs
-  CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b"
-  "CLetrec \<equiv> \<Lambda> F. csnd\<cdot>(F\<cdot>(\<mu> x. cfst\<cdot>(F\<cdot>x)))"
+definition
+  CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
+  "CLetrec = (\<Lambda> F. csnd\<cdot>(F\<cdot>(\<mu> x. cfst\<cdot>(F\<cdot>x))))"
 
 nonterminals
   recbinds recbindt recbind
@@ -181,12 +181,12 @@
 
 translations
   (recbindt) "x = a, \<langle>y,ys\<rangle> = \<langle>b,bs\<rangle>" == (recbindt) "\<langle>x,y,ys\<rangle> = \<langle>a,b,bs\<rangle>"
-  (recbindt) "x = a, y = b"           == (recbindt) "\<langle>x,y\<rangle> = \<langle>a,b\<rangle>"
+  (recbindt) "x = a, y = b"          == (recbindt) "\<langle>x,y\<rangle> = \<langle>a,b\<rangle>"
 
 translations
   "_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
-  "Letrec xs = a in \<langle>e,es\<rangle>"    == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
-  "Letrec xs = a in e"         == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
+  "Letrec xs = a in \<langle>e,es\<rangle>"    == "CONST CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
+  "Letrec xs = a in e"         == "CONST CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
 
 text {*
   Bekic's Theorem: Simultaneous fixed points over pairs
@@ -222,9 +222,9 @@
 
 subsection {* Weak admissibility *}
 
-constdefs
-  admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
-  "admw P \<equiv> \<forall>F. (\<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)) \<longrightarrow> P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
+definition
+  admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "admw P = (\<forall>F. (\<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)) \<longrightarrow> P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>))"
 
 text {* an admissible formula is also weak admissible *}
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Fixrec.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -21,11 +21,13 @@
   fail :: "'a maybe"
   "fail \<equiv> Abs_maybe (sinl\<cdot>ONE)"
 
-  return :: "'a \<rightarrow> 'a maybe"
+constdefs
+  return :: "'a \<rightarrow> 'a maybe" where
   "return \<equiv> \<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x))"
 
-  maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo"
-  "maybe_when \<equiv> \<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m)"
+definition
+  maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo" where
+  "maybe_when = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m))"
 
 lemma maybeE:
   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
@@ -57,14 +59,14 @@
                   cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
 
 translations
-  "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
+  "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
 
 
 subsubsection {* Monadic bind operator *}
 
-constdefs
-  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
-  "bind \<equiv> \<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x"
+definition
+  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" where
+  "bind = (\<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x)"
 
 text {* monad laws *}
 
@@ -86,9 +88,9 @@
 
 subsubsection {* Run operator *}
 
-constdefs
-  run:: "'a maybe \<rightarrow> 'a::pcpo"
-  "run \<equiv> maybe_when\<cdot>\<bottom>\<cdot>ID"
+definition
+  run:: "'a maybe \<rightarrow> 'a::pcpo" where
+  "run = maybe_when\<cdot>\<bottom>\<cdot>ID"
 
 text {* rewrite rules for run *}
 
@@ -103,12 +105,13 @@
 
 subsubsection {* Monad plus operator *}
 
-constdefs
-  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
-  "mplus \<equiv> \<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | return\<cdot>x \<Rightarrow> m1"
+definition
+  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" where
+  "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | return\<cdot>x \<Rightarrow> m1)"
 
-syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
-translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
+abbreviation
+  mplus_syn :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe"  (infixr "+++" 65)  where
+  "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2"
 
 text {* rewrite rules for mplus *}
 
@@ -129,14 +132,13 @@
 
 subsubsection {* Fatbar combinator *}
 
-constdefs
-  fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)"
-  "fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x"
+definition
+  fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)" where
+  "fatbar = (\<Lambda> a b x. a\<cdot>x +++ b\<cdot>x)"
 
-syntax
-  "\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)
-translations
-  "m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2"
+abbreviation
+  fatbar_syn :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)  where
+  "m1 \<parallel> m2 == fatbar\<cdot>m1\<cdot>m2"
 
 lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
 by (simp add: fatbar_def)
@@ -201,15 +203,15 @@
   "_var" :: "'a"
 
 translations
-  "_Case1 p r" => "branch (_pat p)\<cdot>(_var p r)"
-  "_var (_args x y) r" => "csplit\<cdot>(_var x (_var y r))"
-  "_var () r" => "unit_when\<cdot>r"
+  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
+  "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
+  "_var () r" => "CONST unit_when\<cdot>r"
 
 parse_translation {*
 (* rewrites (_pat x) => (return) *)
 (* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
   [("_pat", K (Syntax.const "Fixrec.return")),
-   mk_binder_tr ("_var", "Abs_CFun")];
+   mk_binder_tr ("_var", @{const_syntax Abs_CFun})];
 *}
 
 text {* Printing Case expressions *}
@@ -219,14 +221,14 @@
 
 print_translation {*
   let
-    fun dest_LAM (Const ("Rep_CFun",_) $ Const ("unit_when",_) $ t) =
-          (Syntax.const "Unity", t)
-    |   dest_LAM (Const ("Rep_CFun",_) $ Const ("csplit",_) $ t) =
+    fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
+          (Syntax.const @{const_syntax Unity}, t)
+    |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
           let
             val (v1, t1) = dest_LAM t;
             val (v2, t2) = dest_LAM t1;
           in (Syntax.const "_args" $ v1 $ v2, t2) end 
-    |   dest_LAM (Const ("Abs_CFun",_) $ t) =
+    |   dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
           let
             val abs = case t of Abs abs => abs
                 | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
@@ -234,11 +236,11 @@
           in (Syntax.const "_var" $ x, t') end
     |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
 
-    fun Case1_tr' [Const("branch",_) $ p, r] =
+    fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
           let val (v, t) = dest_LAM r;
           in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
 
-  in [("Rep_CFun", Case1_tr')] end;
+  in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
 *}
 
 translations
@@ -249,67 +251,74 @@
 
 types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"
 
-constdefs
-  cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat"
-  "cpair_pat p1 p2 \<equiv> \<Lambda>\<langle>x, y\<rangle>.
-    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>))"
+definition
+  cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
+  "cpair_pat p1 p2 = (\<Lambda>\<langle>x, y\<rangle>.
+    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>)))"
 
+definition
   spair_pat ::
-  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat"
-  "spair_pat p1 p2 \<equiv> \<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>"
+  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" where
+  "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>)"
 
-  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
-  "sinl_pat p \<equiv> sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
+definition
+  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
+  "sinl_pat p = sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
 
-  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
-  "sinr_pat p \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
+definition
+  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
+  "sinr_pat p = sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
 
-  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat"
-  "up_pat p \<equiv> fup\<cdot>p"
+definition
+  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" where
+  "up_pat p = fup\<cdot>p"
 
-  TT_pat :: "(tr, unit) pat"
-  "TT_pat \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
+definition
+  TT_pat :: "(tr, unit) pat" where
+  "TT_pat = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
 
-  FF_pat :: "(tr, unit) pat"
-  "FF_pat \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
+definition
+  FF_pat :: "(tr, unit) pat" where
+  "FF_pat = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
 
-  ONE_pat :: "(one, unit) pat"
-  "ONE_pat \<equiv> \<Lambda> ONE. return\<cdot>()"
+definition
+  ONE_pat :: "(one, unit) pat" where
+  "ONE_pat = (\<Lambda> ONE. return\<cdot>())"
 
 text {* Parse translations (patterns) *}
 translations
-  "_pat (cpair\<cdot>x\<cdot>y)" => "cpair_pat (_pat x) (_pat y)"
-  "_pat (spair\<cdot>x\<cdot>y)" => "spair_pat (_pat x) (_pat y)"
-  "_pat (sinl\<cdot>x)" => "sinl_pat (_pat x)"
-  "_pat (sinr\<cdot>x)" => "sinr_pat (_pat x)"
-  "_pat (up\<cdot>x)" => "up_pat (_pat x)"
-  "_pat TT" => "TT_pat"
-  "_pat FF" => "FF_pat"
-  "_pat ONE" => "ONE_pat"
+  "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
+  "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
+  "_pat (CONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
+  "_pat (CONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
+  "_pat (CONST up\<cdot>x)" => "CONST up_pat (_pat x)"
+  "_pat (CONST TT)" => "CONST TT_pat"
+  "_pat (CONST FF)" => "CONST FF_pat"
+  "_pat (CONST ONE)" => "CONST ONE_pat"
 
 text {* Parse translations (variables) *}
 translations
-  "_var (cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
-  "_var (spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
-  "_var (sinl\<cdot>x) r" => "_var x r"
-  "_var (sinr\<cdot>x) r" => "_var x r"
-  "_var (up\<cdot>x) r" => "_var x r"
-  "_var TT r" => "_var () r"
-  "_var FF r" => "_var () r"
-  "_var ONE r" => "_var () r"
+  "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+  "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+  "_var (CONST sinl\<cdot>x) r" => "_var x r"
+  "_var (CONST sinr\<cdot>x) r" => "_var x r"
+  "_var (CONST up\<cdot>x) r" => "_var x r"
+  "_var (CONST TT) r" => "_var () r"
+  "_var (CONST FF) r" => "_var () r"
+  "_var (CONST ONE) r" => "_var () r"
 
 text {* Print translations *}
 translations
-  "cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
-      <= "_match (cpair_pat p1 p2) (_args v1 v2)"
-  "spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
-      <= "_match (spair_pat p1 p2) (_args v1 v2)"
-  "sinl\<cdot>(_match p1 v1)" <= "_match (sinl_pat p1) v1"
-  "sinr\<cdot>(_match p1 v1)" <= "_match (sinr_pat p1) v1"
-  "up\<cdot>(_match p1 v1)" <= "_match (up_pat p1) v1"
-  "TT" <= "_match TT_pat ()"
-  "FF" <= "_match FF_pat ()"
-  "ONE" <= "_match ONE_pat ()"
+  "CONST cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
+      <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
+  "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
+      <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"
+  "CONST sinl\<cdot>(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1"
+  "CONST sinr\<cdot>(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1"
+  "CONST up\<cdot>(_match p1 v1)" <= "_match (CONST up_pat p1) v1"
+  "CONST TT" <= "_match (CONST TT_pat) ()"
+  "CONST FF" <= "_match (CONST FF_pat) ()"
+  "CONST ONE" <= "_match (CONST ONE_pat) ()"
 
 lemma cpair_pat1:
   "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
@@ -382,21 +391,23 @@
   "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
   "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
 
-constdefs
-  wild_pat :: "'a \<rightarrow> unit maybe"
-  "wild_pat \<equiv> \<Lambda> x. return\<cdot>()"
+definition
+  wild_pat :: "'a \<rightarrow> unit maybe" where
+  "wild_pat = (\<Lambda> x. return\<cdot>())"
 
-  as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe"
-  "as_pat p \<equiv> \<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>)"
+definition
+  as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
+  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>))"
 
-  lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)"
-  "lazy_pat p \<equiv> \<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x))"
+definition
+  lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
+  "lazy_pat p = (\<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x)))"
 
 text {* Parse translations (patterns) *}
 translations
-  "_pat _" => "wild_pat"
-  "_pat (_as_pat x y)" => "as_pat (_pat y)"
-  "_pat (_lazy_pat x)" => "lazy_pat (_pat x)"
+  "_pat _" => "CONST wild_pat"
+  "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
+  "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
 
 text {* Parse translations (variables) *}
 translations
@@ -406,13 +417,13 @@
 
 text {* Print translations *}
 translations
-  "_" <= "_match wild_pat ()"
-  "_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)"
-  "_lazy_pat (_match p v)" <= "_match (lazy_pat p) v"
+  "_" <= "_match (CONST wild_pat) ()"
+  "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_var x) v)"
+  "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
 
 text {* Lazy patterns in lambda abstractions *}
 translations
-  "_cabs (_lazy_pat p) r" == "run oo (_Case1 (_lazy_pat p) r)"
+  "_cabs (_lazy_pat p) r" == "CONST run oo (_Case1 (_lazy_pat p) r)"
 
 lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
 by (simp add: branch_def wild_pat_def)
@@ -436,33 +447,41 @@
 
 defaultsort pcpo
 
-constdefs
-  match_UU :: "'a \<rightarrow> unit maybe"
-  "match_UU \<equiv> \<Lambda> x. fail"
+definition
+  match_UU :: "'a \<rightarrow> unit maybe" where
+  "match_UU = (\<Lambda> x. fail)"
+
+definition
+  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe" where
+  "match_cpair = csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
 
-  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
-  "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
+definition
+  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe" where
+  "match_spair = ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
 
-  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
-  "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
-
-  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
-  "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
+definition
+  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe" where
+  "match_sinl = sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
 
-  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
-  "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
+definition
+  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe" where
+  "match_sinr = sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
 
-  match_up :: "'a::cpo u \<rightarrow> 'a maybe"
-  "match_up \<equiv> fup\<cdot>return"
+definition
+  match_up :: "'a::cpo u \<rightarrow> 'a maybe" where
+  "match_up = fup\<cdot>return"
 
-  match_ONE :: "one \<rightarrow> unit maybe"
-  "match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
+definition
+  match_ONE :: "one \<rightarrow> unit maybe" where
+  "match_ONE = (\<Lambda> ONE. return\<cdot>())"
  
-  match_TT :: "tr \<rightarrow> unit maybe"
-  "match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
+definition
+  match_TT :: "tr \<rightarrow> unit maybe" where
+  "match_TT = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
  
-  match_FF :: "tr \<rightarrow> unit maybe"
-  "match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
+definition
+  match_FF :: "tr \<rightarrow> unit maybe" where
+  "match_FF = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
 
 lemma match_UU_simps [simp]:
   "match_UU\<cdot>x = fail"
@@ -532,13 +551,6 @@
 lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
 by simp
 
-ML {*
-val cpair_equalI = thm "cpair_equalI";
-val cpair_eqD1 = thm "cpair_eqD1";
-val cpair_eqD2 = thm "cpair_eqD2";
-val ssubst_lhs = thm "ssubst_lhs";
-val branch_def = thm "branch_def";
-*}
 
 subsection {* Initializing the fixrec package *}
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOLCF/IOA/ABP/Correctness.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -20,22 +20,23 @@
                               then reduce xs
                               else (x#(reduce xs))))"
 
-constdefs
+definition
   abs where
-    "abs  ==
+    "abs  =
       (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
        (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
 
-  system_ioa       :: "('m action, bool * 'm impl_state)ioa"
-  "system_ioa == (env_ioa || impl_ioa)"
+definition
+  system_ioa :: "('m action, bool * 'm impl_state)ioa" where
+  "system_ioa = (env_ioa || impl_ioa)"
 
-  system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
-  "system_fin_ioa == (env_ioa || impl_fin_ioa)"
+definition
+  system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" where
+  "system_fin_ioa = (env_ioa || impl_fin_ioa)"
 
 
-axioms
-
-  sys_IOA:     "IOA system_ioa"
+axiomatization where
+  sys_IOA: "IOA system_ioa" and
   sys_fin_IOA: "IOA system_fin_ioa"
 
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/ABP/Env.thy
--- a/src/HOLCF/IOA/ABP/Env.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Env.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -12,30 +12,32 @@
 types
   'm env_state = bool   -- {* give next bit to system *}
 
-constdefs
-env_asig   :: "'m action signature"
-"env_asig == ({Next},
-               UN m. {S_msg(m)},
-               {})"
+definition
+  env_asig :: "'m action signature" where
+  "env_asig == ({Next},
+                 UN m. {S_msg(m)},
+                 {})"
 
-env_trans  :: "('m action, 'm env_state)transition set"
-"env_trans ==
- {tr. let s = fst(tr);
-          t = snd(snd(tr))
-      in case fst(snd(tr))
-      of
-      Next       => t=True |
-      S_msg(m)   => s=True & t=False |
-      R_msg(m)   => False |
-      S_pkt(pkt) => False |
-      R_pkt(pkt) => False |
-      S_ack(b)   => False |
-      R_ack(b)   => False}"
+definition
+  env_trans :: "('m action, 'm env_state)transition set" where
+  "env_trans =
+   {tr. let s = fst(tr);
+            t = snd(snd(tr))
+        in case fst(snd(tr))
+        of
+        Next       => t=True |
+        S_msg(m)   => s=True & t=False |
+        R_msg(m)   => False |
+        S_pkt(pkt) => False |
+        R_pkt(pkt) => False |
+        S_ack(b)   => False |
+        R_ack(b)   => False}"
 
-env_ioa    :: "('m action, 'm env_state)ioa"
-"env_ioa == (env_asig, {True}, env_trans,{},{})"
+definition
+  env_ioa :: "('m action, 'm env_state)ioa" where
+  "env_ioa = (env_asig, {True}, env_trans,{},{})"
 
-consts
-  "next"     :: "'m env_state => bool"
+axiomatization
+  "next" :: "'m env_state => bool"
 
 end
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/ABP/Impl.thy
--- a/src/HOLCF/IOA/ABP/Impl.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Impl.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -13,21 +13,24 @@
   'm impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
   (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
 
-constdefs
+definition
+ impl_ioa :: "('m action, 'm impl_state)ioa" where
+ "impl_ioa = (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
 
- impl_ioa    :: "('m action, 'm impl_state)ioa"
- "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
-
- sen         :: "'m impl_state => 'm sender_state"
- "sen == fst"
+definition
+ sen :: "'m impl_state => 'm sender_state" where
+ "sen = fst"
 
- rec         :: "'m impl_state => 'm receiver_state"
- "rec == fst o snd"
+definition
+ rec :: "'m impl_state => 'm receiver_state" where
+ "rec = fst o snd"
 
- srch        :: "'m impl_state => 'm packet list"
- "srch == fst o snd o snd"
+definition
+ srch :: "'m impl_state => 'm packet list" where
+ "srch = fst o snd o snd"
 
- rsch        :: "'m impl_state => bool list"
- "rsch == snd o snd o snd"
+definition
+ rsch :: "'m impl_state => bool list" where
+ "rsch = snd o snd o snd"
 
 end
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/ABP/Impl_finite.thy
--- a/src/HOLCF/IOA/ABP/Impl_finite.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Impl_finite.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -14,22 +14,25 @@
     = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
 (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
 
-constdefs
+definition
+  impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where
+  "impl_fin_ioa = (sender_ioa || receiver_ioa || srch_fin_ioa ||
+                  rsch_fin_ioa)"
 
- impl_fin_ioa    :: "('m action, 'm impl_fin_state)ioa"
- "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
-                   rsch_fin_ioa)"
-
- sen_fin         :: "'m impl_fin_state => 'm sender_state"
- "sen_fin == fst"
+definition
+  sen_fin :: "'m impl_fin_state => 'm sender_state" where
+  "sen_fin = fst"
 
- rec_fin         :: "'m impl_fin_state => 'm receiver_state"
- "rec_fin == fst o snd"
+definition
+  rec_fin :: "'m impl_fin_state => 'm receiver_state" where
+  "rec_fin = fst o snd"
 
- srch_fin        :: "'m impl_fin_state => 'm packet list"
- "srch_fin == fst o snd o snd"
+definition
+  srch_fin :: "'m impl_fin_state => 'm packet list" where
+  "srch_fin = fst o snd o snd"
 
- rsch_fin        :: "'m impl_fin_state => bool list"
- "rsch_fin == snd o snd o snd"
+definition
+  rsch_fin :: "'m impl_fin_state => bool list" where
+  "rsch_fin = snd o snd o snd"
 
 end
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/ABP/Packet.thy
--- a/src/HOLCF/IOA/ABP/Packet.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Packet.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -12,11 +12,12 @@
 types
   'msg packet = "bool * 'msg"
 
-constdefs
-  hdr  :: "'msg packet => bool"
-  "hdr == fst"
+definition
+  hdr :: "'msg packet => bool" where
+  "hdr = fst"
 
-  msg :: "'msg packet => 'msg"
-  "msg == snd"
+definition
+  msg :: "'msg packet => 'msg" where
+  "msg = snd"
 
 end
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/ABP/Receiver.thy
--- a/src/HOLCF/IOA/ABP/Receiver.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Receiver.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -12,43 +12,47 @@
 types
   'm receiver_state = "'m list * bool"  -- {* messages, mode *}
 
-constdefs
-  rq            :: "'m receiver_state => 'm list"
-  "rq == fst"
+definition
+  rq :: "'m receiver_state => 'm list" where
+  "rq = fst"
 
-  rbit          :: "'m receiver_state => bool"
-  "rbit == snd"
+definition
+  rbit :: "'m receiver_state => bool" where
+  "rbit = snd"
 
-receiver_asig :: "'m action signature"
-"receiver_asig ==
-  (UN pkt. {R_pkt(pkt)},
-  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
-  {})"
+definition
+  receiver_asig :: "'m action signature" where
+  "receiver_asig =
+    (UN pkt. {R_pkt(pkt)},
+    (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
+    {})"
 
-receiver_trans :: "('m action, 'm receiver_state)transition set"
-"receiver_trans ==
- {tr. let s = fst(tr);
-          t = snd(snd(tr))
-      in
-      case fst(snd(tr))
-      of
-      Next    =>  False |
-      S_msg(m) => False |
-      R_msg(m) => (rq(s) ~= [])  &
-                   m = hd(rq(s))  &
-                   rq(t) = tl(rq(s))   &
-                  rbit(t)=rbit(s)  |
-      S_pkt(pkt) => False |
-      R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
-                         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
-                         rq(t) =rq(s) & rbit(t)=rbit(s)  |
-      S_ack(b) => b = rbit(s)                        &
-                      rq(t) = rq(s)                    &
-                      rbit(t)=rbit(s) |
-      R_ack(b) => False}"
+definition
+  receiver_trans :: "('m action, 'm receiver_state)transition set" where
+  "receiver_trans =
+   {tr. let s = fst(tr);
+            t = snd(snd(tr))
+        in
+        case fst(snd(tr))
+        of
+        Next    =>  False |
+        S_msg(m) => False |
+        R_msg(m) => (rq(s) ~= [])  &
+                     m = hd(rq(s))  &
+                     rq(t) = tl(rq(s))   &
+                    rbit(t)=rbit(s)  |
+        S_pkt(pkt) => False |
+        R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
+                           rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
+                           rq(t) =rq(s) & rbit(t)=rbit(s)  |
+        S_ack(b) => b = rbit(s)                        &
+                        rq(t) = rq(s)                    &
+                        rbit(t)=rbit(s) |
+        R_ack(b) => False}"
 
-receiver_ioa :: "('m action, 'm receiver_state)ioa"
-"receiver_ioa ==
- (receiver_asig, {([],False)}, receiver_trans,{},{})"
+definition
+  receiver_ioa :: "('m action, 'm receiver_state)ioa" where
+  "receiver_ioa =
+   (receiver_asig, {([],False)}, receiver_trans,{},{})"
 
 end
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/ABP/Sender.thy
--- a/src/HOLCF/IOA/ABP/Sender.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Sender.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -12,41 +12,45 @@
 types
   'm sender_state = "'m list  *  bool"  -- {* messages, Alternating Bit *}
 
-constdefs
-sq            :: "'m sender_state => 'm list"
-"sq == fst"
+definition
+  sq :: "'m sender_state => 'm list" where
+  "sq = fst"
 
-sbit          :: "'m sender_state => bool"
-"sbit == snd"
+definition
+  sbit :: "'m sender_state => bool" where
+  "sbit = snd"
 
-sender_asig   :: "'m action signature"
-"sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
-                  UN pkt. {S_pkt(pkt)},
-                  {})"
+definition
+  sender_asig :: "'m action signature" where
+  "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
+                   UN pkt. {S_pkt(pkt)},
+                   {})"
 
-sender_trans  :: "('m action, 'm sender_state)transition set"
-"sender_trans ==
- {tr. let s = fst(tr);
-          t = snd(snd(tr))
-      in case fst(snd(tr))
-      of
-      Next     => if sq(s)=[] then t=s else False |
-      S_msg(m) => sq(t)=sq(s)@[m]   &
-                  sbit(t)=sbit(s)  |
-      R_msg(m) => False |
-      S_pkt(pkt) => sq(s) ~= []  &
-                     hdr(pkt) = sbit(s)      &
-                    msg(pkt) = hd(sq(s))    &
-                    sq(t) = sq(s)           &
-                    sbit(t) = sbit(s) |
-      R_pkt(pkt) => False |
-      S_ack(b)   => False |
-      R_ack(b)   => if b = sbit(s) then
-                     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
-                     sq(t)=sq(s) & sbit(t)=sbit(s)}"
-
-sender_ioa    :: "('m action, 'm sender_state)ioa"
-"sender_ioa ==
- (sender_asig, {([],True)}, sender_trans,{},{})"
+definition
+  sender_trans :: "('m action, 'm sender_state)transition set" where
+  "sender_trans =
+   {tr. let s = fst(tr);
+            t = snd(snd(tr))
+        in case fst(snd(tr))
+        of
+        Next     => if sq(s)=[] then t=s else False |
+        S_msg(m) => sq(t)=sq(s)@[m]   &
+                    sbit(t)=sbit(s)  |
+        R_msg(m) => False |
+        S_pkt(pkt) => sq(s) ~= []  &
+                       hdr(pkt) = sbit(s)      &
+                      msg(pkt) = hd(sq(s))    &
+                      sq(t) = sq(s)           &
+                      sbit(t) = sbit(s) |
+        R_pkt(pkt) => False |
+        S_ack(b)   => False |
+        R_ack(b)   => if b = sbit(s) then
+                       sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
+                       sq(t)=sq(s) & sbit(t)=sbit(s)}"
+  
+definition
+  sender_ioa :: "('m action, 'm sender_state)ioa" where
+  "sender_ioa =
+   (sender_asig, {([],True)}, sender_trans,{},{})"
 
 end
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/Modelcheck/Ring3.thy
--- a/src/HOLCF/IOA/Modelcheck/Ring3.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -11,9 +11,9 @@
   Zero_One token | One_Two token | Two_Zero token |
   Leader_Zero | Leader_One | Leader_Two
 
-constdefs
-  Greater :: "[token, token] => bool"
-  "Greater x y ==
+definition
+  Greater :: "[token, token] => bool" where
+  "Greater x y =
     (x~=Leader & x~=id0 & y=id0) | (x=id4 & y~=id4 & y~=Leader) |
     (x=id2 & y=id1) | (x=id3 & y=id1) | (x=id3 & y=id2)"
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/NTP/Correctness.thy
--- a/src/HOLCF/IOA/NTP/Correctness.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -9,10 +9,10 @@
 imports Impl Spec
 begin
 
-constdefs
-  hom :: "'m impl_state => 'm list"
-  "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
-                           else tl(sq(sen s)))"
+definition
+  hom :: "'m impl_state => 'm list" where
+  "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
+                         else tl(sq(sen s)))"
 
 ML_setup {*
 (* repeated from Traces.ML *)
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/NTP/Packet.thy
--- a/src/HOLCF/IOA/NTP/Packet.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Packet.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -10,12 +10,12 @@
 types
   'msg packet = "bool * 'msg"
 
-constdefs
-
-  hdr  :: "'msg packet => bool"
+definition
+  hdr :: "'msg packet => bool" where
   "hdr == fst"
 
-  msg :: "'msg packet => 'msg"
+definition
+  msg :: "'msg packet => 'msg" where
   "msg == snd"
 
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOLCF/IOA/Storage/Correctness.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/Storage/Correctness.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -11,13 +11,13 @@
 
 defaultsort type
 
-constdefs
-  sim_relation   :: "((nat * bool) * (nat set * bool)) set"
-  "sim_relation == {qua. let c = fst qua; a = snd qua ;
-                             k = fst c;   b = snd c;
-                             used = fst a; c = snd a
-                         in
-                         (! l:used. l < k) & b=c }"
+definition
+  sim_relation :: "((nat * bool) * (nat set * bool)) set" where
+  "sim_relation = {qua. let c = fst qua; a = snd qua ;
+                            k = fst c;   b = snd c;
+                            used = fst a; c = snd a
+                        in
+                        (! l:used. l < k) & b=c}"
 
 declare split_paired_All [simp]
 declare split_paired_Ex [simp del]
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -68,23 +68,6 @@
   rename_set    :: "'a set => ('c => 'a option) => 'c set"
   rename        :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
 
-
-syntax
-
-  "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"  ("_ -_--_-> _" [81,81,81,81] 100)
-  "act"        :: "('a,'s)ioa => 'a set"
-  "ext"        :: "('a,'s)ioa => 'a set"
-  "int"        :: "('a,'s)ioa => 'a set"
-  "inp"        :: "('a,'s)ioa => 'a set"
-  "out"        :: "('a,'s)ioa => 'a set"
-  "local"      :: "('a,'s)ioa => 'a set"
-
-
-syntax (xsymbols)
-
-  "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"
-                  ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
-
 notation (xsymbols)
   par  (infixr "\<parallel>" 10)
 
@@ -96,15 +79,19 @@
     reachable_0:  "s : starts_of C ==> reachable C s"
   | reachable_n:  "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t"
 
+abbreviation
+  trans_of_syn  ("_ -_--_-> _" [81,81,81,81] 100) where
+  "s -a--A-> t == (s,a,t):trans_of A"
 
-translations
-  "s -a--A-> t"   == "(s,a,t):trans_of A"
-  "act A"         == "actions (asig_of A)"
-  "ext A"         == "externals (asig_of A)"
-  "int A"         == "internals (asig_of A)"
-  "inp A"         == "inputs (asig_of A)"
-  "out A"         == "outputs (asig_of A)"
-  "local A"       == "locals (asig_of A)"
+notation (xsymbols)
+  trans_of_syn  ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
+
+abbreviation "act A == actions (asig_of A)"
+abbreviation "ext A == externals (asig_of A)"
+abbreviation int where "int A == internals (asig_of A)"
+abbreviation "inp A == inputs (asig_of A)"
+abbreviation "out A == outputs (asig_of A)"
+abbreviation "local A == locals (asig_of A)"
 
 defs
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -27,24 +27,23 @@
 
   Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"
 
-syntax
+abbreviation
+  Consq_syn  ("(_/>>_)"  [66,65] 65) where
+  "a>>s == Consq a$s"
 
- "@Consq"         ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
- (* list Enumeration *)
-  "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
-  "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
+notation (xsymbols)
+  Consq_syn  ("(_\<leadsto>_)"  [66,65] 65)
 
 
-syntax (xsymbols)
-  "@Consq"     ::"'a => 'a Seq => 'a Seq"       ("(_\<leadsto>_)"  [66,65] 65)
-
-
+(* list Enumeration *)
+syntax
+  "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
+  "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
 translations
-  "a>>s"         == "Consq a$s"
   "[x, xs!]"     == "x>>[xs!]"
-  "[x!]"         == "x>>nil"
+  "[x!]"         == "x>>CONST nil"
   "[x, xs?]"     == "x>>[xs?]"
-  "[x?]"         == "x>>UU"
+  "[x?]"         == "x>>CONST UU"
 
 defs
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOLCF/IOA/meta_theory/TL.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -30,10 +30,10 @@
 Next         ::"'a temporal => 'a temporal"
 Leadsto      ::"'a temporal => 'a temporal => 'a temporal"  (infixr "~>" 22)
 
-syntax (xsymbols)
-   "Box"        ::"'a temporal => 'a temporal"   ("\<box> (_)" [80] 80)
-   "Diamond"    ::"'a temporal => 'a temporal"   ("\<diamond> (_)" [80] 80)
-   "Leadsto"    ::"'a temporal => 'a temporal => 'a temporal"  (infixr "\<leadsto>" 22)
+notation (xsymbols)
+  Box  ("\<box> (_)" [80] 80) and
+  Diamond  ("\<diamond> (_)" [80] 80) and
+  Leadsto  (infixr "\<leadsto>" 22)
 
 defs
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Lift.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -16,9 +16,9 @@
 
 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
 
-constdefs
-  Def :: "'a \<Rightarrow> 'a lift"
-  "Def x \<equiv> Abs_lift (up\<cdot>(Discr x))"
+definition
+  Def :: "'a \<Rightarrow> 'a lift" where
+  "Def x = Abs_lift (up\<cdot>(Discr x))"
 
 subsection {* Lift as a datatype *}
 
@@ -110,15 +110,17 @@
 
 subsection {* Further operations *}
 
-constdefs
-  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10)
-  "flift1 \<equiv> \<lambda>f. (\<Lambda> x. lift_case \<bottom> f x)"
+definition
+  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
+  "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
 
-  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)"
-  "flift2 f \<equiv> FLIFT x. Def (f x)"
+definition
+  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
+  "flift2 f = (FLIFT x. Def (f x))"
 
-  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift"
-  "liftpair x \<equiv> csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
+definition
+  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift" where
+  "liftpair x = csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
 
 subsection {* Continuity Proofs for flift1, flift2 *}
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/One.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -12,13 +12,12 @@
 begin
 
 types one = "unit lift"
+translations
+  "one" <= (type) "unit lift" 
 
 constdefs
   ONE :: "one"
-  "ONE \<equiv> Def ()"
-
-translations
-  "one" <= (type) "unit lift" 
+  "ONE == Def ()"
 
 text {* Exhaustion and Elimination for type @{typ one} *}
 
@@ -50,13 +49,13 @@
 
 text {* Case analysis function for type @{typ one} *}
 
-constdefs
-  one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a"
-  "one_when \<equiv> \<Lambda> a. strictify\<cdot>(\<Lambda> _. a)"
+definition
+  one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
+  "one_when = (\<Lambda> a. strictify\<cdot>(\<Lambda> _. a))"
 
 translations
-  "case x of ONE \<Rightarrow> t" == "one_when\<cdot>t\<cdot>x"
-  "\<Lambda> ONE. t" == "one_when\<cdot>t"
+  "case x of CONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
+  "\<Lambda> (CONST ONE). t" == "CONST one_when\<cdot>t"
 
 lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
 by (simp add: one_when_def)
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Pcpo.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -171,12 +171,12 @@
 axclass pcpo < cpo
   least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
 
-constdefs
-  UU :: "'a::pcpo"
-  "UU \<equiv> THE x. \<forall>y. x \<sqsubseteq> y"
+definition
+  UU :: "'a::pcpo" where
+  "UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
 
-syntax (xsymbols)
-  UU :: "'a::pcpo" ("\<bottom>")
+notation (xsymbols)
+  UU  ("\<bottom>")
 
 text {* derive the old rule minimal *}
  
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Porder.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -22,7 +22,7 @@
 
 axclass po < sq_ord
   refl_less [iff]: "x \<sqsubseteq> x"
-  antisym_less:    "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"    
+  antisym_less:    "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
   trans_less:      "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
 
 text {* minimal fixes least element *}
@@ -58,32 +58,38 @@
 
 subsection {* Chains and least upper bounds *}
 
-constdefs  
+text {* class definitions *}
 
-  -- {* class definitions *}
-  is_ub :: "['a set, 'a::po] \<Rightarrow> bool"       (infixl "<|" 55)
-  "S <| x \<equiv> \<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x"
+definition
+  is_ub :: "['a set, 'a::po] \<Rightarrow> bool"  (infixl "<|" 55)  where
+  "(S <| x) = (\<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x)"
 
-  is_lub :: "['a set, 'a::po] \<Rightarrow> bool"       (infixl "<<|" 55)
-  "S <<| x \<equiv> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
+definition
+  is_lub :: "['a set, 'a::po] \<Rightarrow> bool"  (infixl "<<|" 55)  where
+  "(S <<| x) = (S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u))"
 
+definition
   -- {* Arbitrary chains are total orders *}
-  tord :: "'a::po set \<Rightarrow> bool"
-  "tord S \<equiv> \<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
+  tord :: "'a::po set \<Rightarrow> bool" where
+  "tord S = (\<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x))"
 
+definition
   -- {* Here we use countable chains and I prefer to code them as functions! *}
-  chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
-  "chain F \<equiv> \<forall>i. F i \<sqsubseteq> F (Suc i)"
+  chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
+  "chain F = (\<forall>i. F i \<sqsubseteq> F (Suc i))"
 
+definition
   -- {* finite chains, needed for monotony of continuous functions *}
-  max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool"
-  "max_in_chain i C \<equiv> \<forall>j. i \<le> j \<longrightarrow> C i = C j" 
+  max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool" where
+  "max_in_chain i C = (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
 
-  finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
-  "finite_chain C \<equiv> chain(C) \<and> (\<exists>i. max_in_chain i C)"
+definition
+  finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
+  "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
 
-  lub :: "'a set \<Rightarrow> 'a::po"
-  "lub S \<equiv> THE x. S <<| x"
+definition
+  lub :: "'a set \<Rightarrow> 'a::po" where
+  "lub S = (THE x. S <<| x)"
 
 abbreviation
   Lub  (binder "LUB " 10) where
@@ -124,8 +130,6 @@
 
 text {* technical lemmas about @{term lub} and @{term is_lub} *}
 
-lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard]
-
 lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
 apply (unfold lub_def)
 apply (rule theI)
@@ -201,7 +205,7 @@
 apply (erule ub_rangeD)
 done
 
-lemma lub_finch2: 
+lemma lub_finch2:
         "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
 apply (unfold finite_chain_def)
 apply (erule conjE)
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Sprod.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -48,10 +48,10 @@
 
 translations
   "(:x, y, z:)" == "(:x, (:y, z:):)"
-  "(:x, y:)"    == "spair\<cdot>x\<cdot>y"
+  "(:x, y:)"    == "CONST spair\<cdot>x\<cdot>y"
 
 translations
-  "\<Lambda>(spair\<cdot>x\<cdot>y). t" == "ssplit\<cdot>(\<Lambda> x y. t)"
+  "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
 
 subsection {* Case analysis *}
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Ssum.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -27,12 +27,13 @@
 
 subsection {* Definitions of constructors *}
 
-constdefs
-  sinl :: "'a \<rightarrow> ('a ++ 'b)"
-  "sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>"
+definition
+  sinl :: "'a \<rightarrow> ('a ++ 'b)" where
+  "sinl = (\<Lambda> a. Abs_Ssum <a, \<bottom>>)"
 
-  sinr :: "'b \<rightarrow> ('a ++ 'b)"
-  "sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>"
+definition
+  sinr :: "'b \<rightarrow> ('a ++ 'b)" where
+  "sinr = (\<Lambda> b. Abs_Ssum <\<bottom>, b>)"
 
 subsection {* Properties of @{term sinl} and @{term sinr} *}
 
@@ -169,11 +170,11 @@
 
 subsection {* Definitions of constants *}
 
-constdefs
-  Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c"
-  "Iwhen \<equiv> \<lambda>f g s.
+definition
+  Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c" where
+  "Iwhen = (\<lambda>f g s.
     if cfst\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then f\<cdot>(cfst\<cdot>(Rep_Ssum s)) else
-    if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>"
+    if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>)"
 
 text {* rewrites for @{term Iwhen} *}
 
@@ -213,16 +214,16 @@
 
 subsection {* Continuous versions of constants *}
 
-constdefs
-  sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c"
-  "sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
+definition
+  sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
+  "sscase = (\<Lambda> f g s. Iwhen f g s)"
 
 translations
-  "case s of sinl\<cdot>x \<Rightarrow> t1 | sinr\<cdot>y \<Rightarrow> t2" == "sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+  "case s of CONST sinl\<cdot>x \<Rightarrow> t1 | CONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
 
 translations
-  "\<Lambda>(sinl\<cdot>x). t" == "sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
-  "\<Lambda>(sinr\<cdot>y). t" == "sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
+  "\<Lambda>(CONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
+  "\<Lambda>(CONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
 
 text {* continuous versions of lemmas for @{term sscase} *}
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Tr.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -28,17 +28,19 @@
   neg    :: "tr \<rightarrow> tr"
   If2    :: "[tr, 'c, 'c] \<Rightarrow> 'c"
 
-syntax
-  "@cifte"   :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60)
-  "@andalso" :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ andalso _" [36,35] 35)
-  "@orelse"  :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ orelse _"  [31,30] 30)
+abbreviation
+  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(3If _/ (then _/ else _) fi)" 60)  where
+  "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
+
+abbreviation
+  andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
+  "x andalso y == trand\<cdot>x\<cdot>y"
+
+abbreviation
+  orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
+  "x orelse y == tror\<cdot>x\<cdot>y"
  
 translations
-  "x andalso y" == "trand\<cdot>x\<cdot>y"
-  "x orelse y"  == "tror\<cdot>x\<cdot>y"
-  "If b then e1 else e2 fi" == "trifte\<cdot>e1\<cdot>e2\<cdot>b"
-
-translations
   "\<Lambda> TT. t" == "trifte\<cdot>t\<cdot>\<bottom>"
   "\<Lambda> FF. t" == "trifte\<cdot>\<bottom>\<cdot>t"
 
diff -r d91391a8705b -r 2c8caac48ade src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Up.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -115,7 +115,7 @@
 by (rule ext, rule up_lemma3 [symmetric])
 
 lemma up_lemma6:
-  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>  
+  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
       \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
 apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
 apply assumption
@@ -197,16 +197,17 @@
 
 subsection {* Continuous versions of constants *}
 
-constdefs  
-  up  :: "'a \<rightarrow> 'a u"
-  "up \<equiv> \<Lambda> x. Iup x"
+definition
+  up  :: "'a \<rightarrow> 'a u" where
+  "up = (\<Lambda> x. Iup x)"
 
-  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
-  "fup \<equiv> \<Lambda> f p. Ifup f p"
+definition
+  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
+  "fup = (\<Lambda> f p. Ifup f p)"
 
 translations
-  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
-  "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
+  "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+  "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
 
 text {* continuous versions of lemmas for @{typ "('a)u"} *}