# HG changeset patch
# User wenzelm
# Date 1140120720 -3600
# Node ID 1b3780be6cc25a2d0e111fb94e1d0636f23d0fd7
# Parent  a1a251b297ddc4606d627902bd051d58f63067f1
new-style definitions/abbreviations;

diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Complex/ex/Sqrt.thy
--- a/src/HOL/Complex/ex/Sqrt.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Complex/ex/Sqrt.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -17,17 +17,17 @@
   theorem.
 *}
 
-constdefs
-  rationals :: "real set"    ("\<rat>")
-  "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
+definition
+  rationals  ("\<rat>")
+  "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
 
-theorem rationals_rep: "x \<in> \<rat> \<Longrightarrow>
-  \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1"
+theorem rationals_rep [elim?]:
+  assumes "x \<in> \<rat>"
+  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd (m, n) = 1"
 proof -
-  assume "x \<in> \<rat>"
-  then obtain m n :: nat where
+  from `x \<in> \<rat>` obtain m n :: nat where
       n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
-    by (unfold rationals_def) blast
+    unfolding rationals_def by blast
   let ?gcd = "gcd (m, n)"
   from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
   let ?k = "m div ?gcd"
@@ -58,14 +58,9 @@
     with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
     with gcd show ?thesis by simp
   qed
-  ultimately show ?thesis by blast
+  ultimately show ?thesis ..
 qed
 
-lemma [elim?]: "r \<in> \<rat> \<Longrightarrow>
-  (\<And>m n. n \<noteq> 0 \<Longrightarrow> \<bar>r\<bar> = real m / real n \<Longrightarrow> gcd (m, n) = 1 \<Longrightarrow> C)
-    \<Longrightarrow> C"
-  using rationals_rep by blast
-
 
 subsection {* Main theorem *}
 
@@ -74,10 +69,11 @@
   irrational.
 *}
 
-theorem sqrt_prime_irrational: "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
+theorem sqrt_prime_irrational:
+  assumes "prime p"
+  shows "sqrt (real p) \<notin> \<rat>"
 proof
-  assume p_prime: "prime p"
-  then have p: "1 < p" by (simp add: prime_def)
+  from `prime p` have p: "1 < p" by (simp add: prime_def)
   assume "sqrt (real p) \<in> \<rat>"
   then obtain m n where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
@@ -94,12 +90,12 @@
   have "p dvd m \<and> p dvd n"
   proof
     from eq have "p dvd m\<twosuperior>" ..
-    with p_prime show "p dvd m" by (rule prime_dvd_power_two)
+    with `prime p` show "p dvd m" by (rule prime_dvd_power_two)
     then obtain k where "m = p * k" ..
     with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
     with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
     then have "p dvd n\<twosuperior>" ..
-    with p_prime show "p dvd n" by (rule prime_dvd_power_two)
+    with `prime p` show "p dvd n" by (rule prime_dvd_power_two)
   qed
   then have "p dvd gcd (m, n)" ..
   with gcd have "p dvd 1" by simp
@@ -119,10 +115,11 @@
   structure, it is probably closer to proofs seen in mathematics.
 *}
 
-theorem "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
+theorem
+  assumes "prime p"
+  shows "sqrt (real p) \<notin> \<rat>"
 proof
-  assume p_prime: "prime p"
-  then have p: "1 < p" by (simp add: prime_def)
+  from `prime p` have p: "1 < p" by (simp add: prime_def)
   assume "sqrt (real p) \<in> \<rat>"
   then obtain m n where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
@@ -134,12 +131,12 @@
   also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
   finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
   then have "p dvd m\<twosuperior>" ..
-  with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
+  with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
   then obtain k where "m = p * k" ..
   with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
   with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
   then have "p dvd n\<twosuperior>" ..
-  with p_prime have "p dvd n" by (rule prime_dvd_power_two)
+  with `prime p` have "p dvd n" by (rule prime_dvd_power_two)
   with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
   with gcd have "p dvd 1" by simp
   then have "p \<le> 1" by (simp add: dvd_imp_le)
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Commutation.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -10,25 +10,24 @@
 
 subsection {* Basic definitions *}
 
-constdefs
+definition
   square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
-  "square R S T U ==
-    \<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U))"
+  "square R S T U =
+    (\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U)))"
 
   commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
-  "commute R S == square R S S R"
+  "commute R S = square R S S R"
 
   diamond :: "('a \<times> 'a) set => bool"
-  "diamond R == commute R R"
+  "diamond R = commute R R"
 
   Church_Rosser :: "('a \<times> 'a) set => bool"
-  "Church_Rosser R ==
-    \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
+  "Church_Rosser R =
+    (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
 
-syntax
+abbreviation (output)
   confluent :: "('a \<times> 'a) set => bool"
-translations
-  "confluent R" == "diamond (R^*)"
+  "confluent R = diamond (R^*)"
 
 
 subsection {* Basic lemmas *}
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Eta.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -21,14 +21,13 @@
 consts
   eta :: "(dB \<times> dB) set"
 
-syntax 
-  "_eta" :: "[dB, dB] => bool"   (infixl "-e>" 50)
-  "_eta_rtrancl" :: "[dB, dB] => bool"   (infixl "-e>>" 50)
-  "_eta_reflcl" :: "[dB, dB] => bool"   (infixl "-e>=" 50)
-translations
-  "s -e> t" == "(s, t) \<in> eta"
-  "s -e>> t" == "(s, t) \<in> eta^*"
-  "s -e>= t" == "(s, t) \<in> eta^="
+abbreviation (output)
+  eta_red :: "[dB, dB] => bool"   (infixl "-e>" 50)
+  "(s -e> t) = ((s, t) \<in> eta)"
+  eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50)
+  "(s -e>> t) = ((s, t) \<in> eta^*)"
+  eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50)
+  "(s -e>= t) = ((s, t) \<in> eta^=)"
 
 inductive eta
   intros
@@ -225,13 +224,12 @@
 consts
   par_eta :: "(dB \<times> dB) set"
 
-syntax 
-  "_par_eta" :: "[dB, dB] => bool"   (infixl "=e>" 50)
-translations
-  "s =e> t" == "(s, t) \<in> par_eta"
+abbreviation (output)
+  par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
+  "(s =e> t) = ((s, t) \<in> par_eta)"
 
 syntax (xsymbols)
-  "_par_eta" :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
+  par_eta_red :: "[dB, dB] => bool"   (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
 
 inductive par_eta
 intros
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -56,15 +56,15 @@
 consts
   beta :: "(dB \<times> dB) set"
 
-syntax
-  "_beta" :: "[dB, dB] => bool"  (infixl "->" 50)
-  "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->>" 50)
+abbreviation (output)
+  beta_red :: "[dB, dB] => bool"  (infixl "->" 50)
+  "(s -> t) = ((s, t) \<in> beta)"
+  beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
+  "(s ->> t) = ((s, t) \<in> beta^*)"
+
 syntax (latex)
-  "_beta" :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
-  "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
-translations
-  "s \<rightarrow>\<^sub>\<beta> t" == "(s, t) \<in> beta"
-  "s \<rightarrow>\<^sub>\<beta>\<^sup>* t" == "(s, t) \<in> beta^*"
+  beta_red :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+  beta_reds :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
 
 inductive beta
   intros
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/ListApplication.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -8,10 +8,9 @@
 
 theory ListApplication imports Lambda begin
 
-syntax
-  "_list_application" :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
-translations
-  "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
+abbreviation (output)
+  list_application :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
+  "t \<degree>\<degree> ts = foldl (op \<degree>) t ts"
 
 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
   by (induct ts rule: rev_induct) auto
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -12,10 +12,9 @@
   Lifting beta-reduction to lists of terms, reducing exactly one element.
 *}
 
-syntax
-  "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
-translations
-  "rs => ss" == "(rs, ss) : step1 beta"
+abbreviation (output)
+  list_beta :: "dB list => dB list => bool"   (infixl "=>" 50)
+  "(rs => ss) = ((rs, ss) : step1 beta)"
 
 lemma head_Var_reduction:
   "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/ListOrder.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -13,9 +13,9 @@
   element.
 *}
 
-constdefs
+definition
   step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
-  "step1 r ==
+  "step1 r =
     {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
       us @ z' # vs}"
 
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -17,10 +17,9 @@
 consts
   par_beta :: "(dB \<times> dB) set"
 
-syntax
-  par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
-translations
-  "s => t" == "(s, t) \<in> par_beta"
+abbreviation (output)
+  par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50)
+  "(s => t) = ((s, t) \<in> par_beta)"
 
 inductive par_beta
   intros
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Type.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -11,9 +11,9 @@
 
 subsection {* Environments *}
 
-constdefs
+definition
   shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
-  "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
+  "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
 syntax (xsymbols)
   shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
 syntax (HTML output)
@@ -47,21 +47,23 @@
   typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
   typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
 
-syntax
-  "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
-  "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
-  "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
+abbreviation (output)
+  funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
+  "Ts =>> T = foldr Fun Ts T"
+
+  typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
+  "(env |- t : T) = ((env, t, T) \<in> typing)"
+
+  typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
     ("_ ||- _ : _" [50, 50, 50] 50)
+  "(env ||- ts : Ts) = typings env ts Ts"
+
 syntax (xsymbols)
-  "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+  typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
 syntax (latex)
-  "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
-  "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
+  funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
+  typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
     ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
-translations
-  "Ts \<Rrightarrow> T" \<rightleftharpoons> "foldr Fun Ts T"
-  "env \<turnstile> t : T" \<rightleftharpoons> "(env, t, T) \<in> typing"
-  "env \<tturnstile> ts : Ts" \<rightleftharpoons> "typings env ts Ts"
 
 inductive typing
   intros
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -16,9 +16,9 @@
 
 subsection {* Terms in normal form *}
 
-constdefs
+definition
   listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-  "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
+  "listall P xs == (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
 
 declare listall_def [extraction_expand]
 
@@ -361,12 +361,11 @@
 consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
   rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
 
-syntax
-  "_rtyping" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
+abbreviation (output)
+  rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
+  "(e |-\<^sub>R t : T) = ((e, t, T) \<in> rtyping)"
 syntax (xsymbols)
-  "_rtyping" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
-translations
-  "e \<turnstile>\<^sub>R t : T" \<rightleftharpoons> "(e, t, T) \<in> rtyping"
+  rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
 
 inductive rtyping
   intros
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Library/Accessible_Part.thy
--- a/src/HOL/Library/Accessible_Part.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Accessible_Part.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -23,10 +23,9 @@
   intros
     accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
 
-syntax
+abbreviation (output)
   termi :: "('a \<times> 'a) set => 'a set"
-translations
-  "termi r" == "acc (r\<inverse>)"
+  "termi r == acc (r\<inverse>)"
 
 
 subsection {* Induction rules *}
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -11,12 +11,9 @@
 
 subsection {* List constructors over the datatype universe *}
 
-constdefs
-  NIL :: "'a Datatype_Universe.item"
-  "NIL \<equiv> Datatype_Universe.In0 (Datatype_Universe.Numb 0)"
-  CONS :: "'a Datatype_Universe.item \<Rightarrow> 'a Datatype_Universe.item
-    \<Rightarrow> 'a Datatype_Universe.item"
-  "CONS M N \<equiv> Datatype_Universe.In1 (Datatype_Universe.Scons M N)"
+definition
+  "NIL = Datatype_Universe.In0 (Datatype_Universe.Numb 0)"
+  "CONS M N = Datatype_Universe.In1 (Datatype_Universe.Scons M N)"
 
 lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL"
   and NIL_not_CONS [iff]: "NIL \<noteq> CONS M N"
@@ -30,9 +27,8 @@
     -- {* A continuity result? *}
   by (simp add: CONS_def In1_UN1 Scons_UN1_y)
 
-constdefs
-  List_case where
-  "List_case c h \<equiv> Datatype_Universe.Case (\<lambda>_. c) (Datatype_Universe.Split h)"
+definition
+  "List_case c h = Datatype_Universe.Case (\<lambda>_. c) (Datatype_Universe.Split h)"
 
 lemma List_case_NIL [simp]: "List_case c h NIL = c"
   and List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
@@ -63,10 +59,8 @@
       None \<Rightarrow> NIL
     | Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
 
-constdefs
-  LList_corec :: "'a \<Rightarrow> ('a \<Rightarrow> ('b Datatype_Universe.item \<times> 'a) option) \<Rightarrow>
-    'b Datatype_Universe.item"
-  "LList_corec a f \<equiv> \<Union>k. LList_corec_aux k f a"
+definition
+  "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
 
 text {*
   Note: the subsequent recursion equation for @{text LList_corec} may
@@ -150,12 +144,9 @@
   finally show ?thesis .
 qed
 
-constdefs
-  LNil :: "'a llist"
-  "LNil \<equiv> Abs_llist NIL"
-
-  LCons :: "'a \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
-  "LCons x xs \<equiv> Abs_llist (CONS (Datatype_Universe.Leaf x) (Rep_llist xs))"
+definition
+  "LNil = Abs_llist NIL"
+  "LCons x xs = Abs_llist (CONS (Datatype_Universe.Leaf x) (Rep_llist xs))"
 
 lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
   apply (simp add: LNil_def LCons_def)
@@ -202,11 +193,9 @@
 qed
 
 
-constdefs
-  llist_case :: "'b \<Rightarrow> ('a \<Rightarrow> 'a llist \<Rightarrow> 'b) \<Rightarrow> 'a llist \<Rightarrow> 'b"
-  "llist_case c d l \<equiv>
+definition
+  "llist_case c d l =
     List_case c (\<lambda>x y. d (inv Datatype_Universe.Leaf x) (Abs_llist y)) (Rep_llist l)"
-
 translations
   "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "llist_case a (\<lambda>x l. b) p"
 
@@ -219,9 +208,8 @@
     CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
 
 
-constdefs
-  llist_corec :: "'a \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> 'b llist"
-  "llist_corec a f \<equiv>
+definition
+  "llist_corec a f =
     Abs_llist (LList_corec a
       (\<lambda>z.
         case f z of None \<Rightarrow> None
@@ -539,8 +527,7 @@
 
 subsubsection {* @{text Lconst} *}
 
-constdefs
-  Lconst where
+definition
   "Lconst M \<equiv> lfp (\<lambda>N. CONS M N)"
 
 lemma Lconst_fun_mono: "mono (CONS M)"
@@ -580,12 +567,9 @@
 
 subsubsection {* @{text Lmap} and @{text lmap} *}
 
-constdefs
-  Lmap where
-  "Lmap f M \<equiv> LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
-
-  lmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a llist \<Rightarrow> 'b llist"
-  "lmap f l \<equiv> llist_corec l
+definition
+  "Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
+  "lmap f l = llist_corec l
     (\<lambda>z.
       case z of LNil \<Rightarrow> None
       | LCons y z \<Rightarrow> Some (f y, z))"
@@ -678,15 +662,12 @@
 
 subsubsection {* @{text Lappend} *}
 
-constdefs
-  Lappend where
-  "Lappend M N \<equiv> LList_corec (M, N)
+definition
+  "Lappend M N = LList_corec (M, N)
     (split (List_case
         (List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2))))
         (\<lambda>M1 M2 N. Some (M1, (M2, N)))))"
-
-  lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
-  "lappend l n \<equiv> llist_corec (l, n)
+  "lappend l n = llist_corec (l, n)
     (split (llist_case
         (llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2))))
         (\<lambda>l1 l2 n. Some (l1, (l2, n)))))"
@@ -760,9 +741,9 @@
 
 text {* @{text llist_fun_equalityI} cannot be used here! *}
 
-constdefs
+definition
   iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
-  "iterates f a \<equiv> llist_corec a (\<lambda>x. Some (x, f x))"
+  "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
 
 lemma iterates: "iterates f x = LCons x (iterates f (f x))"
   apply (unfold iterates_def)
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -155,9 +155,9 @@
 
 subsection {* Parallel lists *}
 
-constdefs
+definition
   parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
-  "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
+  "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
 
 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
   unfolding parallel_def by blast
@@ -215,9 +215,9 @@
 
 subsection {* Postfix order on lists *}
 
-constdefs
+definition
   postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50)
-  "xs >>= ys == \<exists>zs. xs = zs @ ys"
+  "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"
 
 lemma postfix_refl [simp, intro!]: "xs >>= xs"
   by (auto simp add: postfix_def)
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -20,29 +20,31 @@
     Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
   and [simp] = Rep_multiset_inject [symmetric]
 
-constdefs
+definition
   Mempty :: "'a multiset"    ("{#}")
-  "{#} == Abs_multiset (\<lambda>a. 0)"
+  "{#} = Abs_multiset (\<lambda>a. 0)"
 
   single :: "'a => 'a multiset"    ("{#_#}")
-  "{#a#} == Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
+  "{#a#} = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
 
   count :: "'a multiset => 'a => nat"
-  "count == Rep_multiset"
+  "count = Rep_multiset"
 
   MCollect :: "'a multiset => ('a => bool) => 'a multiset"
-  "MCollect M P == Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
+  "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
+
+abbreviation (output)
+  Melem :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
+  "(a :# M) = (0 < count M a)"
 
 syntax
-  "_Melem" :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
   "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ : _./ _#})")
 translations
-  "a :# M" == "0 < count M a"
   "{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
 
-constdefs
+definition
   set_of :: "'a multiset => 'a set"
-  "set_of M == {x. x :# M}"
+  "set_of M = {x. x :# M}"
 
 instance multiset :: (type) "{plus, minus, zero}" ..
 
@@ -52,9 +54,9 @@
   Zero_multiset_def [simp]: "0 == {#}"
   size_def: "size M == setsum (count M) (set_of M)"
 
-constdefs
- multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
- "multiset_inter A B \<equiv> A - (A - B)"
+definition
+  multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
+  "multiset_inter A B = A - (A - B)"
 
 
 text {*
@@ -377,14 +379,14 @@
 
 subsubsection {* Well-foundedness *}
 
-constdefs
+definition
   mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
-  "mult1 r ==
+  "mult1 r =
     {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
       (\<forall>b. b :# K --> (b, a) \<in> r)}"
 
   mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
-  "mult r == (mult1 r)\<^sup>+"
+  "mult r = (mult1 r)\<^sup>+"
 
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   by (simp add: mult1_def)
@@ -793,16 +795,9 @@
 
 subsection {* Pointwise ordering induced by count *}
 
-consts
-  mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"
-
-syntax
-  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50)
-translations
-  "x \<le># y" == "mset_le x y"
-
-defs
-  mset_le_def: "xs \<le># ys == (\<forall>a. count xs a \<le> count ys a)"
+definition
+  mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50)
+  "(xs \<le># ys) = (\<forall>a. count xs a \<le> count ys a)"
 
 lemma mset_le_refl[simp]: "xs \<le># xs"
   unfolding mset_le_def by auto
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Primes.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -10,12 +10,12 @@
 imports Main
 begin
 
-constdefs
+definition
   coprime :: "nat => nat => bool"
-  "coprime m n == gcd (m, n) = 1"
+  "coprime m n = (gcd (m, n) = 1)"
 
   prime :: "nat \<Rightarrow> bool"
-  "prime p == 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)"
+  "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
 
 lemma two_is_prime: "prime 2"
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Quotient.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -74,9 +74,9 @@
  representation of elements of a quotient type.
 *}
 
-constdefs
+definition
   "class" :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
-  "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
+  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
 
 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
 proof (cases A)
@@ -133,9 +133,9 @@
 
 subsection {* Picking representing elements *}
 
-constdefs
+definition
   pick :: "'a::equiv quot => 'a"
-  "pick A == SOME a. A = \<lfloor>a\<rfloor>"
+  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
 
 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
 proof (unfold pick_def)
diff -r a1a251b297dd -r 1b3780be6cc2 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Unix/Unix.thy	Thu Feb 16 21:12:00 2006 +0100
@@ -160,15 +160,13 @@
   \cite{Nipkow-et-al:2000:HOL}.
 *}
 
-constdefs
-  attributes :: "file \<Rightarrow> att"
-  "attributes file \<equiv>
+definition
+  "attributes file =
     (case file of
       Val (att, text) \<Rightarrow> att
     | Env att dir \<Rightarrow> att)"
 
-  attributes_update :: "att \<Rightarrow> file \<Rightarrow> file"
-  "attributes_update att file \<equiv>
+  "attributes_update att file =
     (case file of
       Val (att', text) \<Rightarrow> Val (att, text)
     | Env att' dir \<Rightarrow> Env att dir)"
@@ -201,9 +199,8 @@
   has user id 0).
 *}
 
-constdefs
-  init :: "uid set \<Rightarrow> file"
-  "init users \<equiv>
+definition
+  "init users =
     Env \<lparr>owner = 0, others = {Readable}\<rparr>
       (\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty)
         else None)"
@@ -223,8 +220,7 @@
   access a file unconditionally (in our simplified model).
 *}
 
-constdefs
-  access :: "file \<Rightarrow> path \<Rightarrow> uid \<Rightarrow> perms \<Rightarrow> file option"
+definition
   "access root path uid perms \<equiv>
     (case lookup root path of
       None \<Rightarrow> None
@@ -648,8 +644,7 @@
   transition.
 *}
 
-constdefs
-  can_exec :: "file \<Rightarrow> operation list \<Rightarrow> bool"
+definition
   "can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'"
 
 lemma can_exec_nil: "can_exec root []"
@@ -843,13 +838,12 @@
   notes facts = user\<^isub>1_known user\<^isub>1_not_root users_neq
     perms\<^isub>1_writable perms\<^isub>2_not_writable
 
-  fixes bogus :: "operation list"
-    and bogus_path :: path
-  defines "bogus \<equiv>
+definition (in situation)
+  "bogus =
      [Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],
       Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],
       Creat user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
-    and "bogus_path \<equiv> [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
+  "bogus_path = [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
 
 text {*
   The @{term bogus} operations are the ones that lead into the uncouth
@@ -867,9 +861,8 @@
   neither owned and nor writable by @{term user\<^isub>1}.
 *}
 
-locale invariant = situation +
-  fixes invariant :: "file \<Rightarrow> path \<Rightarrow> bool"
-  defines "invariant root path \<equiv>
+definition (in situation)
+  "invariant root path \<equiv>
     (\<exists>att dir.
       access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
       user\<^isub>1 \<noteq> owner att \<and>
@@ -907,7 +900,7 @@
   we just have to inspect rather special cases.
 *}
 
-lemma (in invariant) cannot_rmdir:
+lemma (in situation) cannot_rmdir:
   assumes inv: "invariant root bogus_path"
     and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
   shows False
@@ -923,7 +916,7 @@
   ultimately show False by (simp add: bogus_path_def)
 qed
 
-lemma (in invariant)
+lemma (in situation)
   assumes init: "init users =bogus\<Rightarrow> root"
   notes eval = facts access_def init_def
   shows init_invariant: "invariant root bogus_path"
@@ -946,7 +939,7 @@
   required here.
 *}
 
-lemma (in invariant) preserve_invariant:
+lemma (in situation) preserve_invariant:
   assumes tr: "root \<midarrow>x\<rightarrow> root'"
     and inv: "invariant root path"
     and uid: "uid_of x = user\<^isub>1"
@@ -1090,8 +1083,7 @@
   overall procedure (see \secref{sec:unix-inv-procedure}).
 *}
 
-corollary result:
-  includes invariant
+corollary (in situation)
   assumes bogus: "init users =bogus\<Rightarrow> root"
   shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and>
     can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))"
@@ -1100,11 +1092,4 @@
     and bogus show ?thesis by (rule general_procedure)
 qed
 
-text {*
-  So this is our final result:
-
-  @{thm [display, show_question_marks = false] result [OF
-  invariant.intro, OF situation.intro]}
-*}
-
 end