# HG changeset patch
# User wenzelm
# Date 1148744522 -7200
# Node ID d8d0f8f51d69d36188ec45ff68bee1fc377e45fa
# Parent  ff13585fbdab7eeacaadb19c6fc29c58c89fb3cc
tuned;

diff -r ff13585fbdab -r d8d0f8f51d69 TFL/post.ML
--- a/TFL/post.ML	Sat May 27 17:42:00 2006 +0200
+++ b/TFL/post.ML	Sat May 27 17:42:02 2006 +0200
@@ -156,7 +156,7 @@
 
 (*lcp: curry the predicate of the induction rule*)
 fun curry_rule rl =
-  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl)), rl);
+  SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
 
 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
 val meta_outer =
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Complex/ex/NSPrimes.thy
--- a/src/HOL/Complex/ex/NSPrimes.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy	Sat May 27 17:42:02 2006 +0200
@@ -13,22 +13,15 @@
 text{*These can be used to derive an alternative proof of the infinitude of
 primes by considering a property of nonstandard sets.*}
 
-
-constdefs
+definition
   hdvd  :: "[hypnat, hypnat] => bool"       (infixl "hdvd" 50)
-   "(M::hypnat) hdvd N == ( *p2* (op dvd)) M N"
-
-declare hdvd_def [transfer_unfold]
+  [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N"
 
-constdefs
   starprime :: "hypnat set"
-  "starprime == ( *s* {p. prime p})"
+  [transfer_unfold]: "starprime = ( *s* {p. prime p})"
 
-declare starprime_def [transfer_unfold]
-
-constdefs
   choicefun :: "'a set => 'a"
-  "choicefun E == (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
+  "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
 
 consts injf_max :: "nat => ('a::{order} set) => 'a"
 primrec
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Complex/ex/Sqrt_Script.thy
--- a/src/HOL/Complex/ex/Sqrt_Script.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Sat May 27 17:42:02 2006 +0200
@@ -52,9 +52,9 @@
 
 subsection {* The set of rational numbers *}
 
-constdefs
+definition
   rationals :: "real set"    ("\<rat>")
-  "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
+  "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
 
 
 subsection {* Main theorem *}
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Com.thy	Sat May 27 17:42:02 2006 +0200
@@ -34,17 +34,14 @@
 
 text{* Execution of commands *}
 consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
-syntax "@exec"  :: "((exp*state) * (nat*state)) set =>
-                    [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
-
-translations  "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
 
-syntax  eval'   :: "[exp*state,nat*state] =>
-                    ((exp*state) * (nat*state)) set => bool"
-                                           ("_/ -|[_]-> _" [50,0,50] 50)
+abbreviation
+  exec_rel  ("_/ -[_]-> _" [50,0,50] 50)
+  "csig -[eval]-> s == (csig,s) \<in> exec eval"
 
-translations
-    "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
+abbreviation (input)
+  generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)
+  "esig -|[eval]-> ns == (esig,ns) \<in> eval"
 
 text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
 inductive "exec eval"
@@ -105,12 +102,12 @@
 subsection {* Expressions *}
 
 text{* Evaluation of arithmetic expressions *}
-consts  eval    :: "((exp*state) * (nat*state)) set"
-       "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
+consts
+  eval    :: "((exp*state) * (nat*state)) set"
 
-translations
-    "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
-    "esig -|-> ns"    == "(esig,ns ) \<in> eval"
+abbreviation
+  eval_rel :: "[exp*state,nat*state] => bool"         (infixl "-|->" 50)
+  "esig -|-> ns == (esig, ns) \<in> eval"
 
 inductive eval
   intros
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/Comb.thy
--- a/src/HOL/Induct/Comb.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Comb.thy	Sat May 27 17:42:02 2006 +0200
@@ -23,7 +23,11 @@
 
 datatype comb = K
               | S
-              | "##" comb comb (infixl 90)
+              | Ap comb comb (infixl "##" 90)
+
+const_syntax (xsymbols)
+  Ap  (infixl "\<bullet>" 90)
+
 
 text {*
   Inductive definition of contractions, @{text "-1->"} and
@@ -32,15 +36,12 @@
 
 consts
   contract  :: "(comb*comb) set"
-  "-1->"    :: "[comb,comb] => bool"   (infixl 50)
-  "--->"    :: "[comb,comb] => bool"   (infixl 50)
 
-translations
-  "x -1-> y" == "(x,y) \<in> contract"
-  "x ---> y" == "(x,y) \<in> contract^*"
-
-syntax (xsymbols)
-  "op ##" :: "[comb,comb] => comb"  (infixl "\<bullet>" 90)
+abbreviation
+  contract_rel1 :: "[comb,comb] => bool"   (infixl "-1->" 50)
+  "x -1-> y == (x,y) \<in> contract"
+  contract_rel :: "[comb,comb] => bool"   (infixl "--->" 50)
+  "x ---> y == (x,y) \<in> contract^*"
 
 inductive contract
   intros
@@ -56,12 +57,12 @@
 
 consts
   parcontract :: "(comb*comb) set"
-  "=1=>"      :: "[comb,comb] => bool"   (infixl 50)
-  "===>"      :: "[comb,comb] => bool"   (infixl 50)
 
-translations
-  "x =1=> y" == "(x,y) \<in> parcontract"
-  "x ===> y" == "(x,y) \<in> parcontract^*"
+abbreviation
+  parcontract_rel1 :: "[comb,comb] => bool"   (infixl "=1=>" 50)
+  "x =1=> y == (x,y) \<in> parcontract"
+  parcontract_rel :: "[comb,comb] => bool"   (infixl "===>" 50)
+  "x ===> y == (x,y) \<in> parcontract^*"
 
 inductive parcontract
   intros
@@ -74,15 +75,15 @@
   Misc definitions.
 *}
 
-constdefs
+definition
   I :: comb
-  "I == S##K##K"
+  "I = S##K##K"
 
   diamond   :: "('a * 'a)set => bool"	
     --{*confluence; Lambda/Commutation treats this more abstractly*}
-  "diamond(r) == \<forall>x y. (x,y) \<in> r --> 
+  "diamond(r) = (\<forall>x y. (x,y) \<in> r --> 
                   (\<forall>y'. (x,y') \<in> r --> 
-                    (\<exists>z. (y,z) \<in> r & (y',z) \<in> r))"
+                    (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))"
 
 
 subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/LFilter.thy
--- a/src/HOL/Induct/LFilter.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/LFilter.thy	Sat May 27 17:42:02 2006 +0200
@@ -19,12 +19,12 @@
 
 declare findRel.intros [intro]
 
-constdefs
+definition
   find    :: "['a => bool, 'a llist] => 'a llist"
-    "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
+  "find p l = (SOME l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p)))"
 
   lfilter :: "['a => bool, 'a llist] => 'a llist"
-    "lfilter p l == llist_corec l (%l. case find p l of
+  "lfilter p l = llist_corec l (%l. case find p l of
                                             LNil => None
                                           | LCons y z => Some(y,z))"
 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/LList.thy	Sat May 27 17:42:02 2006 +0200
@@ -46,48 +46,48 @@
   'a llist = "llist(range Leaf) :: 'a item set"
   by (blast intro: llist.NIL_I)
 
-constdefs
+definition
   list_Fun   :: "['a item set, 'a item set] => 'a item set"
     --{*Now used exclusively for abbreviating the coinduction rule*}
-     "list_Fun A X == {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
+     "list_Fun A X = {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
 
   LListD_Fun :: 
       "[('a item * 'a item)set, ('a item * 'a item)set] => 
        ('a item * 'a item)set"
-    "LListD_Fun r X ==   
+    "LListD_Fun r X =   
        {z. z = (NIL, NIL) |   
            (\<exists>M N a b. z = (CONS a M, CONS b N) & (a, b) \<in> r & (M, N) \<in> X)}"
 
   LNil :: "'a llist"
      --{*abstract constructor*}
-    "LNil == Abs_LList NIL"
+    "LNil = Abs_LList NIL"
 
   LCons :: "['a, 'a llist] => 'a llist"
      --{*abstract constructor*}
-    "LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
+    "LCons x xs = Abs_LList(CONS (Leaf x) (Rep_LList xs))"
 
   llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
-    "llist_case c d l == 
+    "llist_case c d l =
        List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
 
   LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item"
-    "LList_corec_fun k f == 
+    "LList_corec_fun k f ==
      nat_rec (%x. {})                         
              (%j r x. case f x of None    => NIL
                                 | Some(z,w) => CONS z (r w)) 
              k"
 
   LList_corec     :: "['a, 'a => ('b item * 'a) option] => 'b item"
-    "LList_corec a f == \<Union>k. LList_corec_fun k f a"
+    "LList_corec a f = (\<Union>k. LList_corec_fun k f a)"
 
   llist_corec     :: "['a, 'a => ('b * 'a) option] => 'b llist"
-    "llist_corec a f == 
+    "llist_corec a f =
        Abs_LList(LList_corec a 
                  (%z. case f z of None      => None
                                 | Some(v,w) => Some(Leaf(v), w)))"
 
   llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
-    "llistD_Fun(r) ==    
+    "llistD_Fun(r) =   
         prod_fun Abs_LList Abs_LList `         
                 LListD_Fun (diag(range Leaf))   
                             (prod_fun Rep_LList Rep_LList ` r)"
@@ -101,27 +101,27 @@
 
 subsubsection{* Sample function definitions.  Item-based ones start with @{text L} *}
 
-constdefs
+definition
   Lmap       :: "('a item => 'b item) => ('a item => 'b item)"
-    "Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
+    "Lmap f M = LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
 
   lmap       :: "('a=>'b) => ('a llist => 'b llist)"
-    "lmap f l == llist_corec l (%z. case z of LNil => None 
+    "lmap f l = llist_corec l (%z. case z of LNil => None 
                                            | LCons y z => Some(f(y), z))"
 
   iterates   :: "['a => 'a, 'a] => 'a llist"
-    "iterates f a == llist_corec a (%x. Some((x, f(x))))"     
+    "iterates f a = llist_corec a (%x. Some((x, f(x))))"     
 
   Lconst     :: "'a item => 'a item"
     "Lconst(M) == lfp(%N. CONS M N)"
 
   Lappend    :: "['a item, 'a item] => 'a item"
-   "Lappend M N == LList_corec (M,N)                                         
+   "Lappend M N = LList_corec (M,N)                                         
      (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2))))) 
                       (%M1 M2 N. Some((M1, (M2,N))))))"
 
   lappend    :: "['a llist, 'a llist] => 'a llist"
-    "lappend l n == llist_corec (l,n)                                         
+    "lappend l n = llist_corec (l,n)                                         
        (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2))))) 
                          (%l1 l2 n. Some((l1, (l2,n))))))"
 
@@ -198,6 +198,7 @@
 declare LList_corec_fun_def [THEN def_nat_rec_0, simp]
         LList_corec_fun_def [THEN def_nat_rec_Suc, simp]
 
+
 subsubsection{* The directions of the equality are proved separately *}
 
 lemma LList_corec_subset1: 
@@ -226,7 +227,7 @@
 
 text{*definitional version of same*}
 lemma def_LList_corec: 
-     "[| !!x. h(x) == LList_corec x f |]      
+     "[| !!x. h(x) = LList_corec x f |]      
       ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
 by (simp add: LList_corec)
 
@@ -652,7 +653,7 @@
 
 text{*definitional version of same*}
 lemma def_llist_corec: 
-     "[| !!x. h(x) == llist_corec x f |] ==>      
+     "[| !!x. h(x) = llist_corec x f |] ==>      
       h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
 by (simp add: llist_corec)
 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Mutil.thy	Sat May 27 17:42:02 2006 +0200
@@ -30,16 +30,15 @@
 
 text {* \medskip Sets of squares of the given colour*}
 
-constdefs
+definition
   coloured :: "nat => (nat \<times> nat) set"
-   "coloured b == {(i, j). (i + j) mod 2 = b}"
+  "coloured b = {(i, j). (i + j) mod 2 = b}"
 
-syntax whites  :: "(nat \<times> nat) set"
-       blacks  :: "(nat \<times> nat) set"
-
-translations
-  "whites" == "coloured 0"
-  "blacks" == "coloured (Suc 0)"
+abbreviation
+  whites  :: "(nat \<times> nat) set"
+  "whites == coloured 0"
+  blacks  :: "(nat \<times> nat) set"
+  "blacks == coloured (Suc 0)"
 
 
 text {* \medskip The union of two disjoint tilings is a tiling *}
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/Ordinals.thy
--- a/src/HOL/Induct/Ordinals.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Ordinals.thy	Sat May 27 17:42:02 2006 +0200
@@ -31,11 +31,11 @@
   "iter f 0 = id"
   "iter f (Suc n) = f \<circ> (iter f n)"
 
-constdefs
+definition
   OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
-  "OpLim F a == Limit (\<lambda>n. F n a)"
+  "OpLim F a = Limit (\<lambda>n. F n a)"
   OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>")
-  "\<Squnion>f == OpLim (iter f)"
+  "\<Squnion>f = OpLim (iter f)"
 
 consts
   cantor :: "ordinal => ordinal => ordinal"
@@ -51,9 +51,9 @@
   "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
   "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
 
-constdefs
+definition
   deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
-  "deriv f == \<nabla>(\<Squnion>f)"
+  "deriv f = \<nabla>(\<Squnion>f)"
 
 consts
   veblen :: "ordinal => ordinal => ordinal"
@@ -62,9 +62,9 @@
   "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
   "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
 
-constdefs
-  "veb a == veblen a Zero"
-  "\<epsilon>\<^isub>0 == veb Zero"
-  "\<Gamma>\<^isub>0 == Limit (\<lambda>n. iter veb n Zero)"
+definition
+  "veb a = veblen a Zero"
+  "\<epsilon>\<^isub>0 = veb Zero"
+  "\<Gamma>\<^isub>0 = Limit (\<lambda>n. iter veb n Zero)"
 
 end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/PropLog.thy	Sat May 27 17:42:02 2006 +0200
@@ -28,10 +28,10 @@
 
 consts
   thms  :: "'a pl set => 'a pl set"
-  "|-"  :: "['a pl set, 'a pl] => bool"   (infixl 50)
 
-translations
-  "H |- p" == "p \<in> thms(H)"
+abbreviation
+  thm_rel :: "['a pl set, 'a pl] => bool"   (infixl "|-" 50)
+  "H |- p == p \<in> thms H"
 
 inductive "thms(H)"
   intros
@@ -72,9 +72,9 @@
   is @{text p}.
 *}
 
-constdefs
+definition
   sat :: "['a pl set, 'a pl] => bool"   (infixl "|=" 50)
-    "H |= p  ==  (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
+    "H |= p  =  (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
 
 
 subsection {* Proof theory of propositional logic *}
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/QuoDataType.thy	Sat May 27 17:42:02 2006 +0200
@@ -22,14 +22,14 @@
 provided the keys are the same.*}
 consts  msgrel :: "(freemsg * freemsg) set"
 
-syntax
-  "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)
-syntax (xsymbols)
-  "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)
-syntax (HTML output)
-  "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)
-translations
-  "X \<sim> Y" == "(X,Y) \<in> msgrel"
+abbreviation
+  msg_rel :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)
+  "X ~~ Y == (X,Y) \<in> msgrel"
+
+const_syntax (xsymbols)
+  msg_rel  (infixl "\<sim>" 50)
+const_syntax (HTML output)
+  msg_rel  (infixl "\<sim>" 50)
 
 text{*The first two rules are the desired equations. The next four rules
 make the equations applicable to subterms. The last two rules are symmetry
@@ -142,20 +142,20 @@
 
 
 text{*The abstract message constructors*}
-constdefs
+definition
   Nonce :: "nat \<Rightarrow> msg"
-  "Nonce N == Abs_Msg(msgrel``{NONCE N})"
+  "Nonce N = Abs_Msg(msgrel``{NONCE N})"
 
   MPair :: "[msg,msg] \<Rightarrow> msg"
-   "MPair X Y ==
+   "MPair X Y =
        Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
 
   Crypt :: "[nat,msg] \<Rightarrow> msg"
-   "Crypt K X ==
+   "Crypt K X =
        Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
 
   Decrypt :: "[nat,msg] \<Rightarrow> msg"
-   "Decrypt K X ==
+   "Decrypt K X =
        Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
 
 
@@ -227,9 +227,9 @@
 
 subsection{*The Abstract Function to Return the Set of Nonces*}
 
-constdefs
+definition
   nonces :: "msg \<Rightarrow> nat set"
-   "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
+   "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
 
 lemma nonces_congruent: "freenonces respects msgrel"
 by (simp add: congruent_def msgrel_imp_eq_freenonces) 
@@ -262,9 +262,9 @@
 
 subsection{*The Abstract Function to Return the Left Part*}
 
-constdefs
+definition
   left :: "msg \<Rightarrow> msg"
-   "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
+   "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
 
 lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
 by (simp add: congruent_def msgrel_imp_eqv_freeleft) 
@@ -296,9 +296,9 @@
 
 subsection{*The Abstract Function to Return the Right Part*}
 
-constdefs
+definition
   right :: "msg \<Rightarrow> msg"
-   "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
+   "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
 
 lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
 by (simp add: congruent_def msgrel_imp_eqv_freeright) 
@@ -431,9 +431,9 @@
 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
 need this function in order to prove discrimination theorems.*}
 
-constdefs
+definition
   discrim :: "msg \<Rightarrow> int"
-   "discrim X == contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
+   "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
 
 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
 by (simp add: congruent_def msgrel_imp_eq_freediscrim) 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Sat May 27 17:42:02 2006 +0200
@@ -20,14 +20,14 @@
 text{*The equivalence relation, which makes PLUS associative.*}
 consts  exprel :: "(freeExp * freeExp) set"
 
-syntax
-  "_exprel" :: "[freeExp, freeExp] => bool"  (infixl "~~" 50)
-syntax (xsymbols)
-  "_exprel" :: "[freeExp, freeExp] => bool"  (infixl "\<sim>" 50)
-syntax (HTML output)
-  "_exprel" :: "[freeExp, freeExp] => bool"  (infixl "\<sim>" 50)
-translations
-  "X \<sim> Y" == "(X,Y) \<in> exprel"
+abbreviation
+  exp_rel :: "[freeExp, freeExp] => bool"  (infixl "~~" 50)
+  "X ~~ Y == (X,Y) \<in> exprel"
+
+const_syntax (xsymbols)
+  exp_rel  (infixl "\<sim>" 50)
+const_syntax (HTML output)
+  exp_rel  (infixl "\<sim>" 50)
 
 text{*The first rule is the desired equation. The next three rules
 make the equations applicable to subterms. The last two rules are symmetry
@@ -159,16 +159,16 @@
 
 text{*The abstract message constructors*}
 
-constdefs
+definition
   Var :: "nat \<Rightarrow> exp"
-  "Var N == Abs_Exp(exprel``{VAR N})"
+  "Var N = Abs_Exp(exprel``{VAR N})"
 
   Plus :: "[exp,exp] \<Rightarrow> exp"
-   "Plus X Y ==
+   "Plus X Y =
        Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})"
 
   FnCall :: "[nat, exp list] \<Rightarrow> exp"
-   "FnCall F Xs ==
+   "FnCall F Xs =
        Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"
 
 
@@ -206,8 +206,9 @@
 subsection{*Every list of abstract expressions can be expressed in terms of a
   list of concrete expressions*}
 
-constdefs Abs_ExpList :: "freeExp list => exp list"
-    "Abs_ExpList Xs == map (%U. Abs_Exp(exprel``{U})) Xs"
+definition
+  Abs_ExpList :: "freeExp list => exp list"
+  "Abs_ExpList Xs = map (%U. Abs_Exp(exprel``{U})) Xs"
 
 lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []"
 by (simp add: Abs_ExpList_def)
@@ -283,9 +284,9 @@
 
 subsection{*The Abstract Function to Return the Set of Variables*}
 
-constdefs
+definition
   vars :: "exp \<Rightarrow> nat set"
-   "vars X == \<Union>U \<in> Rep_Exp X. freevars U"
+  "vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
 
 lemma vars_respects: "freevars respects exprel"
 by (simp add: congruent_def exprel_imp_eq_freevars) 
@@ -349,9 +350,9 @@
 
 subsection{*Injectivity of @{term FnCall}*}
 
-constdefs
+definition
   fun :: "exp \<Rightarrow> nat"
-   "fun X == contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
+  "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
 
 lemma fun_respects: "(%U. {freefun U}) respects exprel"
 by (simp add: congruent_def exprel_imp_eq_freefun) 
@@ -361,9 +362,9 @@
 apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects])
 done
 
-constdefs
+definition
   args :: "exp \<Rightarrow> exp list"
-   "args X == contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
+  "args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
 
 text{*This result can probably be generalized to arbitrary equivalence
 relations, but with little benefit here.*}
@@ -396,9 +397,9 @@
 text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
 function in order to prove discrimination theorems.*}
 
-constdefs
+definition
   discrim :: "exp \<Rightarrow> int"
-   "discrim X == contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
+  "discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
 
 lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
 by (simp add: congruent_def exprel_imp_eq_freediscrim) 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/SList.thy	Sat May 27 17:42:02 2006 +0200
@@ -36,12 +36,12 @@
 
 
 (* Defining the Concrete Constructors *)
-constdefs
+definition
   NIL  :: "'a item"
-   "NIL == In0(Numb(0))"
+   "NIL = In0(Numb(0))"
 
   CONS :: "['a item, 'a item] => 'a item"
-   "CONS M N == In1(Scons M N)"
+   "CONS M N = In1(Scons M N)"
 
 consts
   list      :: "'a item set => 'a item set"
@@ -55,12 +55,12 @@
   'a list = "list(range Leaf) :: 'a item set" 
   by (blast intro: list.NIL_I)
 
-constdefs
+definition
   List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
-   "List_case c d == Case(%x. c)(Split(d))"
+   "List_case c d = Case(%x. c)(Split(d))"
   
   List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
-   "List_rec M c d == wfrec (trancl pred_sexp)
+   "List_rec M c d = wfrec (trancl pred_sexp)
                             (%g. List_case c (%x y. d x y (g y))) M"
 
 
@@ -72,20 +72,20 @@
 
 (*Declaring the abstract list constructors*)
 
-constdefs
+definition
   Nil       :: "'a list"
-   "Nil  == Abs_List(NIL)"
+   "Nil  = Abs_List(NIL)"
 
   "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65)
-   "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"
+   "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
 
   (* list Recursion -- the trancl is Essential; see list.ML *)
   list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
-   "list_rec l c d ==
+   "list_rec l c d =
       List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
 
   list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
-   "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+   "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
 
 (* list Enumeration *)
 consts
@@ -110,83 +110,82 @@
   
 (* Generalized Map Functionals *)
 
-constdefs
+definition
   Rep_map   :: "('b => 'a item) => ('b list => 'a item)"
-   "Rep_map f xs == list_rec xs  NIL(%x l r. CONS(f x) r)"
+   "Rep_map f xs = list_rec xs  NIL(%x l r. CONS(f x) r)"
 
   Abs_map   :: "('a item => 'b) => 'a item => 'b list"
-   "Abs_map g M  == List_rec M Nil (%N L r. g(N)#r)"
+   "Abs_map g M  = List_rec M Nil (%N L r. g(N)#r)"
 
 
 (**** Function definitions ****)
 
-constdefs
+definition
 
   null      :: "'a list => bool"
-  "null xs  == list_rec xs True (%x xs r. False)"
+  "null xs  = list_rec xs True (%x xs r. False)"
 
   hd        :: "'a list => 'a"
-  "hd xs    == list_rec xs (@x. True) (%x xs r. x)"
+  "hd xs    = list_rec xs (@x. True) (%x xs r. x)"
 
   tl        :: "'a list => 'a list"
-  "tl xs    == list_rec xs (@xs. True) (%x xs r. xs)"
+  "tl xs    = list_rec xs (@xs. True) (%x xs r. xs)"
 
   (* a total version of tl: *)
   ttl       :: "'a list => 'a list"
-  "ttl xs   == list_rec xs [] (%x xs r. xs)"
+  "ttl xs   = list_rec xs [] (%x xs r. xs)"
 
   member :: "['a, 'a list] => bool"    (infixl "mem" 55)
-  "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"
+  "x mem xs = list_rec xs False (%y ys r. if y=x then True else r)"
 
   list_all  :: "('a => bool) => ('a list => bool)"
-  "list_all P xs == list_rec xs True(%x l r. P(x) & r)"
+  "list_all P xs = list_rec xs True(%x l r. P(x) & r)"
 
   map       :: "('a=>'b) => ('a list => 'b list)"
-  "map f xs == list_rec xs [] (%x l r. f(x)#r)"
+  "map f xs = list_rec xs [] (%x l r. f(x)#r)"
 
 
-constdefs
   append    :: "['a list, 'a list] => 'a list"   (infixr "@" 65)
-  "xs@ys == list_rec xs ys (%x l r. x#r)"
+  "xs@ys = list_rec xs ys (%x l r. x#r)"
 
   filter    :: "['a => bool, 'a list] => 'a list"
-  "filter P xs == list_rec xs []  (%x xs r. if P(x)then x#r else r)"
+  "filter P xs = list_rec xs []  (%x xs r. if P(x)then x#r else r)"
 
   foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
-  "foldl f a xs == list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"
+  "foldl f a xs = list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"
 
   foldr     :: "[['a,'b] => 'b, 'b, 'a list] => 'b"
-  "foldr f a xs     == list_rec xs a (%x xs r. (f x r))"
+  "foldr f a xs     = list_rec xs a (%x xs r. (f x r))"
 
   length    :: "'a list => nat"
-  "length xs== list_rec xs 0 (%x xs r. Suc r)"
+  "length xs = list_rec xs 0 (%x xs r. Suc r)"
 
   drop      :: "['a list,nat] => 'a list"
-  "drop t n == (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"
+  "drop t n = (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"
 
   copy      :: "['a, nat] => 'a list"      (* make list of n copies of x *)
-  "copy t   == nat_rec [] (%m xs. t # xs)"
+  "copy t   = nat_rec [] (%m xs. t # xs)"
 
   flat      :: "'a list list => 'a list"
-  "flat     == foldr (op @) []"
+  "flat     = foldr (op @) []"
 
   nth       :: "[nat, 'a list] => 'a"
-  "nth      == nat_rec hd (%m r xs. r(tl xs))"
+  "nth      = nat_rec hd (%m r xs. r(tl xs))"
 
   rev       :: "'a list => 'a list"
-  "rev xs   == list_rec xs [] (%x xs xsa. xsa @ [x])"
+  "rev xs   = list_rec xs [] (%x xs xsa. xsa @ [x])"
 
 (* miscellaneous definitions *)
   zipWith   :: "['a * 'b => 'c, 'a list * 'b list] => 'c list"
-  "zipWith f S == (list_rec (fst S)  (%T.[])
+  "zipWith f S = (list_rec (fst S)  (%T.[])
                             (%x xs r. %T. if null T then [] 
                                           else f(x,hd T) # r(tl T)))(snd(S))"
 
   zip       :: "'a list * 'b list => ('a*'b) list"
-  "zip      == zipWith  (%s. s)"
+  "zip      = zipWith  (%s. s)"
 
   unzip     :: "('a*'b) list => ('a list * 'b list)"
-  "unzip    == foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
+  "unzip    = foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
 
 
 consts take      :: "['a list,nat] => 'a list"
@@ -425,9 +424,9 @@
     "[| M: sexp;  N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
 by (simp add: Abs_map_def)
 
-(*Eases the use of primitive recursion.  NOTE USE OF == *)
+(*Eases the use of primitive recursion.*)
 lemma def_list_rec_NilCons:
-    "[| !!xs. f(xs) == list_rec xs c h  |] 
+    "[| !!xs. f(xs) = list_rec xs c h  |] 
      ==> f [] = c & f(x#xs) = h x xs (f xs)"
 by simp 
 
@@ -475,11 +474,11 @@
 (** nth **)
 
 lemma def_nat_rec_0_eta:
-    "[| !!n. f == nat_rec c h |] ==> f(0) = c"
+    "[| !!n. f = nat_rec c h |] ==> f(0) = c"
 by simp
 
 lemma def_nat_rec_Suc_eta:
-    "[| !!n. f == nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
+    "[| !!n. f = nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
 by simp
 
 declare def_nat_rec_0_eta [OF nth_def, simp]
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/Sexp.thy
--- a/src/HOL/Induct/Sexp.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Sexp.thy	Sat May 27 17:42:02 2006 +0200
@@ -17,20 +17,20 @@
     NumbI:  "Numb(i) \<in> sexp"
     SconsI: "[| M \<in> sexp;  N \<in> sexp |] ==> Scons M N \<in> sexp"
 
-constdefs
+definition
 
   sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
                 'a item] => 'b"
-   "sexp_case c d e M == THE z. (EX x.   M=Leaf(x) & z=c(x))  
+   "sexp_case c d e M = (THE z. (EX x.   M=Leaf(x) & z=c(x))  
                             | (EX k.   M=Numb(k) & z=d(k))  
-                            | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2)"
+                            | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2))"
 
   pred_sexp :: "('a item * 'a item)set"
-     "pred_sexp == \<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)}"
+     "pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})"
 
   sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
                 ['a item, 'a item, 'b, 'b]=>'b] => 'b"
-   "sexp_rec M c d e == wfrec pred_sexp
+   "sexp_rec M c d e = wfrec pred_sexp
              (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
 
 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Tree.thy	Sat May 27 17:42:02 2006 +0200
@@ -71,12 +71,12 @@
   ordinals.  Start with a predecessor relation and form its transitive 
   closure. *} 
 
-constdefs
+definition
   brouwer_pred :: "(brouwer * brouwer) set"
-  "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
+  "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
 
   brouwer_order :: "(brouwer * brouwer) set"
-  "brouwer_order == brouwer_pred^+"
+  "brouwer_order = brouwer_pred^+"
 
 lemma wf_brouwer_pred: "wf brouwer_pred"
   by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Lattice/Bounds.thy
--- a/src/HOL/Lattice/Bounds.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Lattice/Bounds.thy	Sat May 27 17:42:02 2006 +0200
@@ -15,18 +15,18 @@
   number of elements.
 *}
 
-constdefs
+definition
   is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-  "is_inf x y inf \<equiv> inf \<sqsubseteq> x \<and> inf \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> inf)"
+  "is_inf x y inf = (inf \<sqsubseteq> x \<and> inf \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> inf))"
 
   is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-  "is_sup x y sup \<equiv> x \<sqsubseteq> sup \<and> y \<sqsubseteq> sup \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> sup \<sqsubseteq> z)"
+  "is_sup x y sup = (x \<sqsubseteq> sup \<and> y \<sqsubseteq> sup \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> sup \<sqsubseteq> z))"
 
   is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
-  "is_Inf A inf \<equiv> (\<forall>x \<in> A. inf \<sqsubseteq> x) \<and> (\<forall>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<longrightarrow> z \<sqsubseteq> inf)"
+  "is_Inf A inf = ((\<forall>x \<in> A. inf \<sqsubseteq> x) \<and> (\<forall>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<longrightarrow> z \<sqsubseteq> inf))"
 
   is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
-  "is_Sup A sup \<equiv> (\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z)"
+  "is_Sup A sup = ((\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z))"
 
 text {*
   These definitions entail the following basic properties of boundary
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Sat May 27 17:42:02 2006 +0200
@@ -31,15 +31,15 @@
   such infimum and supremum elements.
 *}
 
-consts
+definition
   Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
+  "Meet A = (THE inf. is_Inf A inf)"
   Join :: "'a::complete_lattice set \<Rightarrow> 'a"
-syntax (xsymbols)
-  Meet :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Sqinter>_" [90] 90)
-  Join :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
-defs
-  Meet_def: "\<Sqinter>A \<equiv> THE inf. is_Inf A inf"
-  Join_def: "\<Squnion>A \<equiv> THE sup. is_Sup A sup"
+  "Join A = (THE sup. is_Sup A sup)"
+
+const_syntax (xsymbols)
+  Meet  ("\<Sqinter>_" [90] 90)
+  Join  ("\<Squnion>_" [90] 90)
 
 text {*
   Due to unique existence of bounds, the complete lattice operations
@@ -142,11 +142,11 @@
   greatest elements.
 *}
 
-constdefs
+definition
   bottom :: "'a::complete_lattice"    ("\<bottom>")
-  "\<bottom> \<equiv> \<Sqinter>UNIV"
+  "\<bottom> = \<Sqinter>UNIV"
   top :: "'a::complete_lattice"    ("\<top>")
-  "\<top> \<equiv> \<Squnion>UNIV"
+  "\<top> = \<Squnion>UNIV"
 
 lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
 proof (unfold bottom_def)
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Sat May 27 17:42:02 2006 +0200
@@ -24,15 +24,15 @@
   infimum and supremum elements.
 *}
 
-consts
+definition
   meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "&&" 70)
+  "x && y = (THE inf. is_inf x y inf)"
   join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "||" 65)
-syntax (xsymbols)
-  meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<sqinter>" 70)
-  join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<squnion>" 65)
-defs
-  meet_def: "x && y \<equiv> THE inf. is_inf x y inf"
-  join_def: "x || y \<equiv> THE sup. is_sup x y sup"
+  "x || y = (THE sup. is_sup x y sup)"
+
+const_syntax (xsymbols)
+  meet  (infixl "\<sqinter>" 70)
+  join  (infixl "\<squnion>" 65)
 
 text {*
   Due to unique existence of bounds, the lattice operations may be
@@ -336,11 +336,11 @@
   are a (degenerate) example of lattice structures.
 *}
 
-constdefs
+definition
   minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
-  "minimum x y \<equiv> (if x \<sqsubseteq> y then x else y)"
+  "minimum x y = (if x \<sqsubseteq> y then x else y)"
   maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
-  "maximum x y \<equiv> (if x \<sqsubseteq> y then y else x)"
+  "maximum x y = (if x \<sqsubseteq> y then y else x)"
 
 lemma is_inf_minimum: "is_inf x y (minimum x y)"
 proof
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Lattice/Orders.thy
--- a/src/HOL/Lattice/Orders.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Lattice/Orders.thy	Sat May 27 17:42:02 2006 +0200
@@ -21,8 +21,8 @@
 axclass leq < type
 consts
   leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
-syntax (xsymbols)
-  leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sqsubseteq>" 50)
+const_syntax (xsymbols)
+  leq  (infixl "\<sqsubseteq>" 50)
 
 axclass quasi_order < leq
   leq_refl [intro?]: "x \<sqsubseteq> x"
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/BigO.thy	Sat May 27 17:42:02 2006 +0200
@@ -38,10 +38,9 @@
 
 subsection {* Definitions *}
 
-constdefs 
-
+definition
   bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
-  "O(f::('a => 'b)) == 
+  "O(f::('a => 'b)) =
       {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
 
 lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
@@ -735,10 +734,10 @@
 
 subsection {* Less than or equal to *}
 
-constdefs 
+definition
   lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
       (infixl "<o" 70)
-  "f <o g == (%x. max (f x - g x) 0)"
+  "f <o g = (%x. max (f x - g x) 0)"
 
 lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
     g =o O(h)"
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Char_ord.thy	Sat May 27 17:42:02 2006 +0200
@@ -13,8 +13,6 @@
 
 consts
   nibble_to_int:: "nibble \<Rightarrow> int"
-  int_to_nibble:: "int \<Rightarrow> nibble"
-
 primrec
   "nibble_to_int Nibble0 = 0"
   "nibble_to_int Nibble1 = 1"
@@ -33,25 +31,25 @@
   "nibble_to_int NibbleE = 14"
   "nibble_to_int NibbleF = 15"
 
-defs
-  int_to_nibble_def:
-    "int_to_nibble x \<equiv> (let y = x mod 16 in
-       if y = 0 then Nibble0 else
-       if y = 1 then Nibble1 else
-       if y = 2 then Nibble2 else
-       if y = 3 then Nibble3 else
-       if y = 4 then Nibble4 else
-       if y = 5 then Nibble5 else
-       if y = 6 then Nibble6 else
-       if y = 7 then Nibble7 else
-       if y = 8 then Nibble8 else
-       if y = 9 then Nibble9 else
-       if y = 10 then NibbleA else
-       if y = 11 then NibbleB else
-       if y = 12 then NibbleC else
-       if y = 13 then NibbleD else
-       if y = 14 then NibbleE else
-       NibbleF)"
+definition
+  int_to_nibble :: "int \<Rightarrow> nibble"
+  "int_to_nibble x \<equiv> (let y = x mod 16 in
+    if y = 0 then Nibble0 else
+    if y = 1 then Nibble1 else
+    if y = 2 then Nibble2 else
+    if y = 3 then Nibble3 else
+    if y = 4 then Nibble4 else
+    if y = 5 then Nibble5 else
+    if y = 6 then Nibble6 else
+    if y = 7 then Nibble7 else
+    if y = 8 then Nibble8 else
+    if y = 9 then Nibble9 else
+    if y = 10 then NibbleA else
+    if y = 11 then NibbleB else
+    if y = 12 then NibbleC else
+    if y = 13 then NibbleD else
+    if y = 14 then NibbleE else
+    NibbleF)"
 
 lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
   by (cases x) (auto simp: int_to_nibble_def Let_def)
@@ -93,15 +91,9 @@
 lemmas char_ord_defs = char_less_def char_le_def
 
 instance char :: order
-  apply intro_classes
-     apply (unfold char_ord_defs)
-     apply (auto simp: char_to_int_pair_eq order_less_le)
-  done
+  by default (auto simp: char_ord_defs char_to_int_pair_eq order_less_le)
 
-instance char::linorder
-  apply intro_classes
-  apply (unfold char_le_def)
-  apply auto
-  done
+instance char :: linorder
+  by default (auto simp: char_le_def)
 
 end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/Commutative_Ring.thy
--- a/src/HOL/Library/Commutative_Ring.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Commutative_Ring.thy	Sat May 27 17:42:02 2006 +0200
@@ -47,16 +47,16 @@
 
 text {* Create polynomial normalized polynomials given normalized inputs. *}
 
-constdefs
+definition
   mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
-  "mkPinj x P \<equiv> (case P of
+  "mkPinj x P = (case P of
     Pc c \<Rightarrow> Pc c |
     Pinj y P \<Rightarrow> Pinj (x + y) P |
     PX p1 y p2 \<Rightarrow> Pinj x P)"
 
-constdefs
+definition
   mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
-  "mkPX P i Q == (case P of
+  "mkPX P i Q = (case P of
     Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
     Pinj j R \<Rightarrow> PX P i Q |
     PX P2 i2 Q2 \<Rightarrow> (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )"
@@ -127,9 +127,9 @@
   "neg (PX P x Q) = PX (neg P) x (neg Q)"
 
 text {* Substraction *}
-constdefs
+definition
   sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
-  "sub p q \<equiv> add (p, neg q)"
+  "sub p q = add (p, neg q)"
 
 text {* Square for Fast Exponentation *}
 primrec
@@ -316,11 +316,6 @@
 qed
 
 
-text {* Code generation *}
-(*
-Does not work, since no generic ring operations implementation is there
-generate_code ("ring.ML") test = "norm"*)
-
 use "comm_ring.ML"
 setup CommRing.setup
 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Continuity.thy	Sat May 27 17:42:02 2006 +0200
@@ -11,9 +11,9 @@
 
 subsection "Chains"
 
-constdefs
+definition
   up_chain :: "(nat => 'a set) => bool"
-  "up_chain F == \<forall>i. F i \<subseteq> F (Suc i)"
+  "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
 
 lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
   by (simp add: up_chain_def)
@@ -21,10 +21,10 @@
 lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
   by (simp add: up_chain_def)
 
-lemma up_chain_less_mono [rule_format]:
-    "up_chain F ==> x < y --> F x \<subseteq> F y"
-  apply (induct_tac y)
-  apply (blast dest: up_chainD elim: less_SucE)+
+lemma up_chain_less_mono:
+    "up_chain F ==> x < y ==> F x \<subseteq> F y"
+  apply (induct y)
+   apply (blast dest: up_chainD elim: less_SucE)+
   done
 
 lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
@@ -33,9 +33,9 @@
   done
 
 
-constdefs
+definition
   down_chain :: "(nat => 'a set) => bool"
-  "down_chain F == \<forall>i. F (Suc i) \<subseteq> F i"
+  "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
 
 lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
   by (simp add: down_chain_def)
@@ -43,10 +43,10 @@
 lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
   by (simp add: down_chain_def)
 
-lemma down_chain_less_mono [rule_format]:
-    "down_chain F ==> x < y --> F y \<subseteq> F x"
-  apply (induct_tac y)
-  apply (blast dest: down_chainD elim: less_SucE)+
+lemma down_chain_less_mono:
+    "down_chain F ==> x < y ==> F y \<subseteq> F x"
+  apply (induct y)
+   apply (blast dest: down_chainD elim: less_SucE)+
   done
 
 lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
@@ -57,9 +57,9 @@
 
 subsection "Continuity"
 
-constdefs
+definition
   up_cont :: "('a set => 'a set) => bool"
-  "up_cont f == \<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F)"
+  "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
 
 lemma up_contI:
     "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
@@ -84,10 +84,10 @@
   done
 
 
-constdefs
+definition
   down_cont :: "('a set => 'a set) => bool"
-  "down_cont f ==
-    \<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F)"
+  "down_cont f =
+    (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
 
 lemma down_contI:
   "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
@@ -114,9 +114,9 @@
 
 subsection "Iteration"
 
-constdefs
+definition
   up_iterate :: "('a set => 'a set) => nat => 'a set"
-  "up_iterate f n == (f^n) {}"
+  "up_iterate f n = (f^n) {}"
 
 lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
   by (simp add: up_iterate_def)
@@ -166,9 +166,9 @@
   done
 
 
-constdefs
+definition
   down_iterate :: "('a set => 'a set) => nat => 'a set"
-  "down_iterate f n == (f^n) UNIV"
+  "down_iterate f n = (f^n) UNIV"
 
 lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   by (simp add: down_iterate_def)
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy	Sat May 27 17:42:02 2006 +0200
@@ -9,15 +9,15 @@
 imports Main
 begin
 
-constdefs
+definition
   Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
-  "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}"
+  "Pi A B = {f. \<forall>x. x \<in> A --> f x \<in> B x}"
 
   extensional :: "'a set => ('a => 'b) set"
-  "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}"
+  "extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}"
 
   "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
-  "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
+  "restrict f A = (%x. if x \<in> A then f x else arbitrary)"
 
 abbreviation
   funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
@@ -27,24 +27,24 @@
   funcset  (infixr "\<rightarrow>" 60)
 
 syntax
-  "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
-  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
+  "_Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
+  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
 
 syntax (xsymbols)
-  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
-  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+  "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
+  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
 
 syntax (HTML output)
-  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
-  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+  "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
+  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
 
 translations
   "PI x:A. B" == "Pi A (%x. B)"
   "%x:A. f" == "restrict (%x. f) A"
 
-constdefs
+definition
   "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
-  "compose A g f == \<lambda>x\<in>A. g (f x)"
+  "compose A g f = (\<lambda>x\<in>A. g (f x))"
 
 
 subsection{*Basic Properties of @{term Pi}*}
@@ -62,7 +62,7 @@
   by (simp add: Pi_def)
 
 lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
-by (auto simp add: Pi_def)
+  by (auto simp add: Pi_def)
 
 lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
 apply (simp add: Pi_def, auto)
@@ -133,7 +133,7 @@
   by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
 
 lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
-  by (auto simp add: restrict_def) 
+  by (auto simp add: restrict_def)
 
 
 subsection{*Bijections Between Sets*}
@@ -141,21 +141,21 @@
 text{*The basic definition could be moved to @{text "Fun.thy"}, but most of
 the theorems belong here, or need at least @{term Hilbert_Choice}.*}
 
-constdefs
-  bij_betw :: "['a => 'b, 'a set, 'b set] => bool"         (*bijective*)
-    "bij_betw f A B == inj_on f A & f ` A = B"
+definition
+  bij_betw :: "['a => 'b, 'a set, 'b set] => bool"         -- {* bijective *}
+  "bij_betw f A B = (inj_on f A & f ` A = B)"
 
 lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
-by (simp add: bij_betw_def)
+  by (simp add: bij_betw_def)
 
 lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
-by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
+  by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
 
 lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
-apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem) 
-apply (simp add: image_compose [symmetric] o_def) 
-apply (simp add: image_def Inv_f_f) 
-done
+  apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
+  apply (simp add: image_compose [symmetric] o_def)
+  apply (simp add: image_def Inv_f_f)
+  done
 
 lemma inj_on_compose:
     "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
@@ -163,9 +163,9 @@
 
 lemma bij_betw_compose:
     "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
-apply (simp add: bij_betw_def compose_eq inj_on_compose)
-apply (auto simp add: compose_def image_def)
-done
+  apply (simp add: bij_betw_def compose_eq inj_on_compose)
+  apply (auto simp add: compose_def image_def)
+  done
 
 lemma bij_betw_restrict_eq [simp]:
      "bij_betw (restrict f A) A B = bij_betw f A B"
@@ -210,13 +210,13 @@
 subsection{*Cardinality*}
 
 lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
-apply (rule card_inj_on_le)
-apply (auto simp add: Pi_def)
-done
+  apply (rule card_inj_on_le)
+    apply (auto simp add: Pi_def)
+  done
 
 lemma card_bij:
      "[|f \<in> A\<rightarrow>B; inj_on f A;
         g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
-by (blast intro: card_inj order_antisym)
+  by (blast intro: card_inj order_antisym)
 
 end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/NatPair.thy
--- a/src/HOL/Library/NatPair.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/NatPair.thy	Sat May 27 17:42:02 2006 +0200
@@ -11,25 +11,24 @@
 begin
 
 text{*
-  An injective function from @{text "\<nat>\<twosuperior>"} to @{text
-  \<nat>}.  Definition and proofs are from \cite[page
-  85]{Oberschelp:1993}.
+  An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}.  Definition
+  and proofs are from \cite[page 85]{Oberschelp:1993}.
 *}
 
-constdefs
+definition
   nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
-  "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
+  "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
 
 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
 proof (cases "2 dvd a")
   case True
-  thus ?thesis by (rule dvd_mult2)
+  then show ?thesis by (rule dvd_mult2)
 next
   case False
-  hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
-  hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
-  hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
-  thus ?thesis by (rule dvd_mult)
+  then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
+  then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
+  then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
+  then show ?thesis by (rule dvd_mult)
 qed
 
 lemma
@@ -37,7 +36,7 @@
   shows nat2_to_nat_help: "u+v \<le> x+y"
 proof (rule classical)
   assume "\<not> ?thesis"
-  hence contrapos: "x+y < u+v"
+  then have contrapos: "x+y < u+v"
     by simp
   have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
     by (unfold nat2_to_nat_def) (simp add: Let_def)
@@ -48,7 +47,7 @@
   proof -
     have "2 dvd (x+y)*Suc(x+y)"
       by (rule dvd2_a_x_suc_a)
-    hence "(x+y)*Suc(x+y) mod 2 = 0"
+    then have "(x+y)*Suc(x+y) mod 2 = 0"
       by (simp only: dvd_eq_mod_eq_0)
     also
     have "2 * Suc(x+y) mod 2 = 0"
@@ -56,7 +55,7 @@
     ultimately have
       "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
       by simp
-    thus ?thesis
+    then show ?thesis
       by simp
   qed
   also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
@@ -75,7 +74,7 @@
 proof -
   {
     fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
-    hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
+    then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
     also from prems [symmetric] have "x+y \<le> u+v"
       by (rule nat2_to_nat_help)
     finally have eq: "u+v = x+y" .
@@ -86,9 +85,9 @@
     with ux have "(u,v) = (x,y)"
       by simp
   }
-  hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
+  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
     by fast
-  thus ?thesis
+  then show ?thesis
     by (unfold inj_on_def) simp
 qed
 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Sat May 27 17:42:02 2006 +0200
@@ -19,20 +19,20 @@
 
 datatype inat = Fin nat | Infty
 
+const_syntax (xsymbols)
+  Infty  ("\<infinity>")
+
+const_syntax (HTML output)
+  Infty  ("\<infinity>")
+
 instance inat :: "{ord, zero}" ..
 
-consts
+definition
   iSuc :: "inat => inat"
-
-syntax (xsymbols)
-  Infty :: inat    ("\<infinity>")
+  "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)"
 
-syntax (HTML output)
-  Infty :: inat    ("\<infinity>")
-
-defs
+defs (overloaded)
   Zero_inat_def: "0 == Fin 0"
-  iSuc_def: "iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
   iless_def: "m < n ==
     case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
     | \<infinity>  => False"
@@ -114,7 +114,6 @@
   by (simp add: inat_defs split:inat_splits, arith?)
 
 
-(* ----------------------------------------------------------------------- *)
 
 lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
   by (simp add: inat_defs split:inat_splits, arith?)
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Product_ord.thy	Sat May 27 17:42:02 2006 +0200
@@ -9,20 +9,19 @@
 imports Main
 begin
 
-instance "*" :: (ord,ord) ord ..
+instance "*" :: (ord, ord) ord ..
 
 defs (overloaded)
-  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)" 
+  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
   prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)"
 
 
 lemmas prod_ord_defs = prod_less_def prod_le_def
 
-instance "*" :: (order,order) order 
-  apply (intro_classes, unfold prod_ord_defs)
-  by (auto intro: order_less_trans)
+instance * :: (order, order) order
+  by default (auto simp: prod_ord_defs intro: order_less_trans)
 
-instance "*":: (linorder,linorder)linorder
-  by (intro_classes, unfold prod_le_def, auto)
+instance * :: (linorder, linorder) linorder
+  by default (auto simp: prod_le_def)
 
-end
\ No newline at end of file
+end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/SetsAndFunctions.thy	Sat May 27 17:42:02 2006 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Library/SetsAndFunctions.thy
-    ID:		$Id$
+    ID:         $Id$
     Author:     Jeremy Avigad and Kevin Donnelly
 *)
 
@@ -9,13 +9,13 @@
 imports Main
 begin
 
-text {* 
+text {*
 This library lifts operations like addition and muliplication to sets and
 functions of appropriate types. It was designed to support asymptotic
 calculations. See the comments at the top of theory @{text BigO}.
 *}
 
-subsection {* Basic definitions *} 
+subsection {* Basic definitions *}
 
 instance set :: (plus) plus ..
 instance fun :: (type, plus) plus ..
@@ -28,14 +28,14 @@
 instance fun :: (type, times) times ..
 
 defs (overloaded)
-  func_times: "f * g == (%x. f x * g x)" 
+  func_times: "f * g == (%x. f x * g x)"
   set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
 
 instance fun :: (type, minus) minus ..
 
 defs (overloaded)
   func_minus: "- f == (%x. - f x)"
-  func_diff: "f - g == %x. f x - g x"                 
+  func_diff: "f - g == %x. f x - g x"
 
 instance fun :: (type, zero) zero ..
 instance set :: (zero) zero ..
@@ -51,12 +51,12 @@
   func_one: "1::(('a::type) => ('b::one)) == %x. 1"
   set_one: "1::('a::one)set == {1}"
 
-constdefs 
+definition
   elt_set_plus :: "'a::plus => 'a set => 'a set"    (infixl "+o" 70)
-  "a +o B == {c. EX b:B. c = a + b}"
+  "a +o B = {c. EX b:B. c = a + b}"
 
   elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
-  "a *o B == {c. EX b:B. c = a * b}"
+  "a *o B = {c. EX b:B. c = a * b}"
 
 abbreviation (input)
   elt_set_eq :: "'a => 'a set => bool"      (infix "=o" 50)
@@ -69,291 +69,292 @@
   by default (auto simp add: func_zero func_plus add_ac)
 
 instance fun :: (type,ab_group_add)ab_group_add
-  apply intro_classes
-  apply (simp add: func_minus func_plus func_zero)
+  apply default
+   apply (simp add: func_minus func_plus func_zero)
   apply (simp add: func_minus func_plus func_diff diff_minus)
-done
+  done
 
 instance fun :: (type,semigroup_mult)semigroup_mult
-  apply intro_classes
+  apply default
   apply (auto simp add: func_times mult_assoc)
-done
+  done
 
 instance fun :: (type,comm_monoid_mult)comm_monoid_mult
-  apply intro_classes
-  apply (auto simp add: func_one func_times mult_ac)
-done
+  apply default
+   apply (auto simp add: func_one func_times mult_ac)
+  done
 
 instance fun :: (type,comm_ring_1)comm_ring_1
-  apply intro_classes
-  apply (auto simp add: func_plus func_times func_minus func_diff ext 
-    func_one func_zero ring_eq_simps) 
+  apply default
+   apply (auto simp add: func_plus func_times func_minus func_diff ext
+     func_one func_zero ring_eq_simps)
   apply (drule fun_cong)
   apply simp
-done
+  done
 
 instance set :: (semigroup_add)semigroup_add
-  apply intro_classes
+  apply default
   apply (unfold set_plus)
   apply (force simp add: add_assoc)
-done
+  done
 
 instance set :: (semigroup_mult)semigroup_mult
-  apply intro_classes
+  apply default
   apply (unfold set_times)
   apply (force simp add: mult_assoc)
-done
+  done
 
 instance set :: (comm_monoid_add)comm_monoid_add
-  apply intro_classes
-  apply (unfold set_plus)
-  apply (force simp add: add_ac)
+  apply default
+   apply (unfold set_plus)
+   apply (force simp add: add_ac)
   apply (unfold set_zero)
   apply force
-done
+  done
 
 instance set :: (comm_monoid_mult)comm_monoid_mult
-  apply intro_classes
-  apply (unfold set_times)
-  apply (force simp add: mult_ac)
+  apply default
+   apply (unfold set_times)
+   apply (force simp add: mult_ac)
   apply (unfold set_one)
   apply force
-done
+  done
+
 
 subsection {* Basic properties *}
 
-lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D" 
-by (auto simp add: set_plus)
+lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
+  by (auto simp add: set_plus)
 
 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
-by (auto simp add: elt_set_plus_def)
+  by (auto simp add: elt_set_plus_def)
 
-lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) + 
-  (b +o D) = (a + b) +o (C + D)"
+lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
+    (b +o D) = (a + b) +o (C + D)"
   apply (auto simp add: elt_set_plus_def set_plus add_ac)
-  apply (rule_tac x = "ba + bb" in exI)
+   apply (rule_tac x = "ba + bb" in exI)
   apply (auto simp add: add_ac)
   apply (rule_tac x = "aa + a" in exI)
   apply (auto simp add: add_ac)
-done
+  done
 
-lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = 
-  (a + b) +o C"
-by (auto simp add: elt_set_plus_def add_assoc)
+lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
+    (a + b) +o C"
+  by (auto simp add: elt_set_plus_def add_assoc)
 
-lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = 
-  a +o (B + C)"
+lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
+    a +o (B + C)"
   apply (auto simp add: elt_set_plus_def set_plus)
-  apply (blast intro: add_ac)
+   apply (blast intro: add_ac)
   apply (rule_tac x = "a + aa" in exI)
   apply (rule conjI)
-  apply (rule_tac x = "aa" in bexI)
-  apply auto
+   apply (rule_tac x = "aa" in bexI)
+    apply auto
   apply (rule_tac x = "ba" in bexI)
-  apply (auto simp add: add_ac)
-done
+   apply (auto simp add: add_ac)
+  done
 
-theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = 
-    a +o (C + D)" 
+theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
+    a +o (C + D)"
   apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus add_ac)
-  apply (rule_tac x = "aa + ba" in exI)
-  apply (auto simp add: add_ac)
-done
+   apply (rule_tac x = "aa + ba" in exI)
+   apply (auto simp add: add_ac)
+  done
 
 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   set_plus_rearrange3 set_plus_rearrange4
 
 lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
-by (auto simp add: elt_set_plus_def)
+  by (auto simp add: elt_set_plus_def)
 
-lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==> 
+lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
     C + E <= D + F"
-by (auto simp add: set_plus)
+  by (auto simp add: set_plus)
 
 lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
-by (auto simp add: elt_set_plus_def set_plus)
+  by (auto simp add: elt_set_plus_def set_plus)
 
-lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==> 
-  a +o D <= D + C" 
-by (auto simp add: elt_set_plus_def set_plus add_ac)
+lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
+    a +o D <= D + C"
+  by (auto simp add: elt_set_plus_def set_plus add_ac)
 
 lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
   apply (subgoal_tac "a +o B <= a +o D")
-  apply (erule order_trans)
-  apply (erule set_plus_mono3)
+   apply (erule order_trans)
+   apply (erule set_plus_mono3)
   apply (erule set_plus_mono)
-done
+  done
 
-lemma set_plus_mono_b: "C <= D ==> x : a +o C 
+lemma set_plus_mono_b: "C <= D ==> x : a +o C
     ==> x : a +o D"
   apply (frule set_plus_mono)
   apply auto
-done
+  done
 
-lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==> 
+lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
     x : D + F"
   apply (frule set_plus_mono2)
-  prefer 2
-  apply force
+   prefer 2
+   apply force
   apply assumption
-done
+  done
 
 lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
   apply (frule set_plus_mono3)
   apply auto
-done
+  done
 
-lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==> 
-  x : a +o D ==> x : D + C" 
+lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
+    x : a +o D ==> x : D + C"
   apply (frule set_plus_mono4)
   apply auto
-done
+  done
 
 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
-by (auto simp add: elt_set_plus_def)
+  by (auto simp add: elt_set_plus_def)
 
 lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
   apply (auto intro!: subsetI simp add: set_plus)
   apply (rule_tac x = 0 in bexI)
-  apply (rule_tac x = x in bexI)
-  apply (auto simp add: add_ac)
-done
+   apply (rule_tac x = x in bexI)
+    apply (auto simp add: add_ac)
+  done
 
 lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
-by (auto simp add: elt_set_plus_def add_ac diff_minus)
+  by (auto simp add: elt_set_plus_def add_ac diff_minus)
 
 lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
   apply (auto simp add: elt_set_plus_def add_ac diff_minus)
   apply (subgoal_tac "a = (a + - b) + b")
-  apply (rule bexI, assumption, assumption)
+   apply (rule bexI, assumption, assumption)
   apply (auto simp add: add_ac)
-done
+  done
 
 lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
-by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus, 
+  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
     assumption)
 
-lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D" 
-by (auto simp add: set_times)
+lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
+  by (auto simp add: set_times)
 
 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
-by (auto simp add: elt_set_times_def)
+  by (auto simp add: elt_set_times_def)
 
-lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) * 
-  (b *o D) = (a * b) *o (C * D)"
+lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
+    (b *o D) = (a * b) *o (C * D)"
   apply (auto simp add: elt_set_times_def set_times)
-  apply (rule_tac x = "ba * bb" in exI)
-  apply (auto simp add: mult_ac)
+   apply (rule_tac x = "ba * bb" in exI)
+   apply (auto simp add: mult_ac)
   apply (rule_tac x = "aa * a" in exI)
   apply (auto simp add: mult_ac)
-done
+  done
 
-lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) = 
-  (a * b) *o C"
-by (auto simp add: elt_set_times_def mult_assoc)
+lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
+    (a * b) *o C"
+  by (auto simp add: elt_set_times_def mult_assoc)
 
-lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C = 
-  a *o (B * C)"
+lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
+    a *o (B * C)"
   apply (auto simp add: elt_set_times_def set_times)
-  apply (blast intro: mult_ac)
+   apply (blast intro: mult_ac)
   apply (rule_tac x = "a * aa" in exI)
   apply (rule conjI)
-  apply (rule_tac x = "aa" in bexI)
-  apply auto
+   apply (rule_tac x = "aa" in bexI)
+    apply auto
   apply (rule_tac x = "ba" in bexI)
-  apply (auto simp add: mult_ac)
-done
+   apply (auto simp add: mult_ac)
+  done
 
-theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) = 
-    a *o (C * D)" 
-  apply (auto intro!: subsetI simp add: elt_set_times_def set_times 
+theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
+    a *o (C * D)"
+  apply (auto intro!: subsetI simp add: elt_set_times_def set_times
     mult_ac)
-  apply (rule_tac x = "aa * ba" in exI)
-  apply (auto simp add: mult_ac)
-done
+   apply (rule_tac x = "aa * ba" in exI)
+   apply (auto simp add: mult_ac)
+  done
 
 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   set_times_rearrange3 set_times_rearrange4
 
 lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
-by (auto simp add: elt_set_times_def)
+  by (auto simp add: elt_set_times_def)
 
-lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==> 
+lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
     C * E <= D * F"
-by (auto simp add: set_times)
+  by (auto simp add: set_times)
 
 lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
-by (auto simp add: elt_set_times_def set_times)
+  by (auto simp add: elt_set_times_def set_times)
 
-lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==> 
-  a *o D <= D * C" 
-by (auto simp add: elt_set_times_def set_times mult_ac)
+lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
+    a *o D <= D * C"
+  by (auto simp add: elt_set_times_def set_times mult_ac)
 
 lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
   apply (subgoal_tac "a *o B <= a *o D")
-  apply (erule order_trans)
-  apply (erule set_times_mono3)
+   apply (erule order_trans)
+   apply (erule set_times_mono3)
   apply (erule set_times_mono)
-done
+  done
 
-lemma set_times_mono_b: "C <= D ==> x : a *o C 
+lemma set_times_mono_b: "C <= D ==> x : a *o C
     ==> x : a *o D"
   apply (frule set_times_mono)
   apply auto
-done
+  done
 
-lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==> 
+lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
     x : D * F"
   apply (frule set_times_mono2)
-  prefer 2
-  apply force
+   prefer 2
+   apply force
   apply assumption
-done
+  done
 
 lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
   apply (frule set_times_mono3)
   apply auto
-done
+  done
 
-lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==> 
-  x : a *o D ==> x : D * C" 
+lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
+    x : a *o D ==> x : D * C"
   apply (frule set_times_mono4)
   apply auto
-done
+  done
 
 lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
-by (auto simp add: elt_set_times_def)
+  by (auto simp add: elt_set_times_def)
 
-lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)= 
-  (a * b) +o (a *o C)"
-by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
+lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
+    (a * b) +o (a *o C)"
+  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
 
-lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) = 
-  (a *o B) + (a *o C)"
+lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
+    (a *o B) + (a *o C)"
   apply (auto simp add: set_plus elt_set_times_def ring_distrib)
-  apply blast
+   apply blast
   apply (rule_tac x = "b + bb" in exI)
   apply (auto simp add: ring_distrib)
-done
+  done
 
-lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <= 
+lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
     a *o D + C * D"
-  apply (auto intro!: subsetI simp add: 
-    elt_set_plus_def elt_set_times_def set_times 
+  apply (auto intro!: subsetI simp add:
+    elt_set_plus_def elt_set_times_def set_times
     set_plus ring_distrib)
   apply auto
-done
+  done
 
 theorems set_times_plus_distribs =
   set_times_plus_distrib
   set_times_plus_distrib2
 
-lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==> 
-    - a : C" 
-by (auto simp add: elt_set_times_def)
+lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
+    - a : C"
+  by (auto simp add: elt_set_times_def)
 
 lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
     - a : (- 1) *o C"
-by (auto simp add: elt_set_times_def)
-  
+  by (auto simp add: elt_set_times_def)
+
 end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Sat May 27 17:42:02 2006 +0200
@@ -35,7 +35,7 @@
   apply blast
   done
 
-constdefs
+definition
   while :: "('a => bool) => ('a => 'a) => 'a => 'a"
   "while b c s == while_aux (b, c, s)"
 
@@ -88,7 +88,8 @@
     and terminate: "!!s. P s ==> \<not> b s ==> Q s"
     and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
   shows "P s \<Longrightarrow> Q (while b c s)"
-  apply (induct s rule: wf [THEN wf_induct])
+  using wf
+  apply (induct s)
   apply simp
   apply (subst while_unfold)
   apply (simp add: invariant terminate)
@@ -101,13 +102,13 @@
       wf r;
       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    Q (while b c s)"
-apply (rule while_rule_lemma)
-prefer 4 apply assumption
-apply blast
-apply blast
-apply(erule wf_subset)
-apply blast
-done
+  apply (rule while_rule_lemma)
+     prefer 4 apply assumption
+    apply blast
+   apply blast
+  apply (erule wf_subset)
+  apply blast
+  done
 
 text {*
  \medskip An application: computation of the @{term lfp} on finite
@@ -142,12 +143,11 @@
 looping because the antisymmetry simproc turns the subset relationship
 back into equality. *}
 
-lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
-  by blast
-
 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
   P {0, 4, 2}"
 proof -
+  have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))"
+    by blast
   have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
     apply blast
     done
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Word.thy	Sat May 27 17:42:02 2006 +0200
@@ -56,17 +56,17 @@
   bitor  :: "bit => bit => bit" (infixr "bitor"  30)
   bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
 
-syntax (xsymbols)
-  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
-  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
-  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
-  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
+const_syntax (xsymbols)
+  bitnot ("\<not>\<^sub>b _" [40] 40)
+  bitand (infixr "\<and>\<^sub>b" 35)
+  bitor  (infixr "\<or>\<^sub>b" 30)
+  bitxor (infixr "\<oplus>\<^sub>b" 30)
 
-syntax (HTML output)
-  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
-  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
-  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
-  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
+const_syntax (HTML output)
+  bitnot ("\<not>\<^sub>b _" [40] 40)
+  bitand (infixr "\<and>\<^sub>b" 35)
+  bitor  (infixr "\<or>\<^sub>b" 30)
+  bitxor (infixr "\<oplus>\<^sub>b" 30)
 
 primrec
   bitnot_zero: "(bitnot \<zero>) = \<one>"
@@ -141,13 +141,13 @@
     by (cases b,auto intro!: zero one)
 qed
 
-constdefs
+definition
   bv_msb :: "bit list => bit"
-  "bv_msb w == if w = [] then \<zero> else hd w"
+  "bv_msb w = (if w = [] then \<zero> else hd w)"
   bv_extend :: "[nat,bit,bit list]=>bit list"
-  "bv_extend i b w == (replicate (i - length w) b) @ w"
+  "bv_extend i b w = (replicate (i - length w) b) @ w"
   bv_not :: "bit list => bit list"
-  "bv_not w == map bitnot w"
+  "bv_not w = map bitnot w"
 
 lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i"
   by (simp add: bv_extend_def)
@@ -176,9 +176,9 @@
 lemma length_bv_not [simp]: "length (bv_not w) = length w"
   by (induct w,simp_all)
 
-constdefs
+definition
   bv_to_nat :: "bit list => nat"
-  "bv_to_nat == foldl (%bn b. 2 * bn + bitval b) 0"
+  "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0"
 
 lemma bv_to_nat_Nil [simp]: "bv_to_nat [] = 0"
   by (simp add: bv_to_nat_def)
@@ -326,9 +326,9 @@
     ..
 qed
 
-constdefs
+definition
   norm_unsigned :: "bit list => bit list"
-  "norm_unsigned == rem_initial \<zero>"
+  "norm_unsigned = rem_initial \<zero>"
 
 lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []"
   by (simp add: norm_unsigned_def)
@@ -349,9 +349,9 @@
   "nat_to_bv_helper n = (%bs. (if n = 0 then bs
                                else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
 
-constdefs
+definition
   nat_to_bv :: "nat => bit list"
-  "nat_to_bv n == nat_to_bv_helper n []"
+  "nat_to_bv n = nat_to_bv_helper n []"
 
 lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
   by (simp add: nat_to_bv_def)
@@ -400,7 +400,7 @@
       assume "k \<le> j" and "j < i"
       with a
       show "P j"
-	by auto
+        by auto
     qed
     show "\<forall> j. k \<le> j \<and> j < i + 1 --> P j"
     proof auto
@@ -409,18 +409,18 @@
       assume ji: "j \<le> i"
       show "P j"
       proof (cases "j = i")
-	assume "j = i"
-	with pi
-	show "P j"
-	  by simp
+        assume "j = i"
+        with pi
+        show "P j"
+          by simp
       next
-	assume "j ~= i"
-	with ji
-	have "j < i"
-	  by simp
-	with kj and a
-	show "P j"
-	  by blast
+        assume "j ~= i"
+        with ji
+        have "j < i"
+          by simp
+        with kj and a
+        show "P j"
+          by blast
       qed
     qed
   qed
@@ -446,39 +446,39 @@
       fix l
       show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
       proof (cases "n < 0")
-	assume "n < 0"
-	thus ?thesis
-	  by (simp add: nat_to_bv_helper.simps)
+        assume "n < 0"
+        thus ?thesis
+          by (simp add: nat_to_bv_helper.simps)
       next
-	assume "~n < 0"
-	show ?thesis
-	proof (rule n_div_2_cases [of n])
-	  assume [simp]: "n = 0"
-	  show ?thesis
-	    apply (simp only: nat_to_bv_helper.simps [of n])
-	    apply simp
-	    done
-	next
-	  assume n2n: "n div 2 < n"
-	  assume [simp]: "0 < n"
-	  hence n20: "0 \<le> n div 2"
-	    by arith
-	  from ind [of "n div 2"] and n2n n20
-	  have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
-	    by blast
-	  show ?thesis
-	    apply (simp only: nat_to_bv_helper.simps [of n])
-	    apply (cases "n=0")
-	    apply simp
-	    apply (simp only: if_False)
-	    apply simp
-	    apply (subst spec [OF ind',of "\<zero>#l"])
-	    apply (subst spec [OF ind',of "\<one>#l"])
-	    apply (subst spec [OF ind',of "[\<one>]"])
-	    apply (subst spec [OF ind',of "[\<zero>]"])
-	    apply simp
-	    done
-	qed
+        assume "~n < 0"
+        show ?thesis
+        proof (rule n_div_2_cases [of n])
+          assume [simp]: "n = 0"
+          show ?thesis
+            apply (simp only: nat_to_bv_helper.simps [of n])
+            apply simp
+            done
+        next
+          assume n2n: "n div 2 < n"
+          assume [simp]: "0 < n"
+          hence n20: "0 \<le> n div 2"
+            by arith
+          from ind [of "n div 2"] and n2n n20
+          have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
+            by blast
+          show ?thesis
+            apply (simp only: nat_to_bv_helper.simps [of n])
+            apply (cases "n=0")
+            apply simp
+            apply (simp only: if_False)
+            apply simp
+            apply (subst spec [OF ind',of "\<zero>#l"])
+            apply (subst spec [OF ind',of "\<one>#l"])
+            apply (subst spec [OF ind',of "[\<one>]"])
+            apply (subst spec [OF ind',of "[\<zero>]"])
+            apply simp
+            done
+        qed
       qed
     qed
   qed
@@ -511,14 +511,14 @@
       fix l2
       show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
       proof -
-	have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
-	  by (induct "length xs",simp_all)
-	hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
-	  bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
-	  by simp
-	also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
-	  by (simp add: ring_distrib)
-	finally show ?thesis .
+        have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
+          by (induct "length xs",simp_all)
+        hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
+          bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
+          by simp
+        also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
+          by (simp add: ring_distrib)
+        finally show ?thesis .
       qed
     qed
   qed
@@ -553,15 +553,15 @@
       apply (simp add: ind' split del: split_if)
       apply (cases "n mod 2 = 0")
       proof simp_all
-	assume "n mod 2 = 0"
-	with mod_div_equality [of n 2]
-	show "n div 2 * 2 = n"
-	  by simp
+        assume "n mod 2 = 0"
+        with mod_div_equality [of n 2]
+        show "n div 2 * 2 = n"
+          by simp
       next
-	assume "n mod 2 = Suc 0"
-	with mod_div_equality [of n 2]
-	show "Suc (n div 2 * 2) = n"
-	  by simp
+        assume "n mod 2 = Suc 0"
+        with mod_div_equality [of n 2]
+        show "Suc (n div 2 * 2) = n"
+          by simp
       qed
   qed
 qed
@@ -715,41 +715,41 @@
       assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
       show "?P xs"
       proof (cases xs)
-	assume [simp]: "xs = []"
-	show ?thesis
-	  by (simp add: nat_to_bv_non0)
+        assume [simp]: "xs = []"
+        show ?thesis
+          by (simp add: nat_to_bv_non0)
       next
-	fix y ys
-	assume [simp]: "xs = y # ys"
-	show ?thesis
-	  apply simp
-	  apply (subst bv_to_nat_dist_append)
-	  apply simp
-	proof -
-	  have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
-	    nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
-	    by (simp add: add_ac mult_ac)
-	  also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
-	    by simp
-	  also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
-	  proof -
-	    from ind
-	    have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
-	      by auto
-	    hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
-	      by simp
-	    show ?thesis
-	      apply (subst nat_helper1)
-	      apply simp_all
-	      done
-	  qed
-	  also have "... = (\<one>#rev ys) @ [y]"
-	    by simp
-	  also have "... = \<one> # rev ys @ [y]"
-	    by simp
-	  finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
-	    .
-	qed
+        fix y ys
+        assume [simp]: "xs = y # ys"
+        show ?thesis
+          apply simp
+          apply (subst bv_to_nat_dist_append)
+          apply simp
+        proof -
+          have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
+            nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
+            by (simp add: add_ac mult_ac)
+          also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
+            by simp
+          also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
+          proof -
+            from ind
+            have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
+              by auto
+            hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
+              by simp
+            show ?thesis
+              apply (subst nat_helper1)
+              apply simp_all
+              done
+          qed
+          also have "... = (\<one>#rev ys) @ [y]"
+            by simp
+          also have "... = \<one> # rev ys @ [y]"
+            by simp
+          finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
+            .
+        qed
       qed
     qed
   qed
@@ -856,9 +856,9 @@
 
 subsection {* Unsigned Arithmetic Operations *}
 
-constdefs
+definition
   bv_add :: "[bit list, bit list ] => bit list"
-  "bv_add w1 w2 == nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
+  "bv_add w1 w2 = nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
 
 lemma bv_add_type1 [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
   by (simp add: bv_add_def)
@@ -893,13 +893,13 @@
     proof
       assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
       hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
-	by (rule add_right_mono)
+        by (rule add_right_mono)
       hence "(2::nat) ^ length w1 \<le> 2 ^ length w2"
-	by simp
+        by simp
       hence "length w1 \<le> length w2"
-	by simp
+        by simp
       thus False
-	by simp
+        by simp
     qed
     thus ?thesis
       by (simp add: diff_mult_distrib2 split: split_max)
@@ -908,9 +908,9 @@
     by arith
 qed
 
-constdefs
+definition
   bv_mult :: "[bit list, bit list ] => bit list"
-  "bv_mult w1 w2 == nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
+  "bv_mult w1 w2 = nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
 
 lemma bv_mult_type1 [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"
   by (simp add: bv_mult_def)
@@ -968,11 +968,11 @@
 
 lemmas [simp del] = norm_signed_Cons
 
-constdefs
+definition
   int_to_bv :: "int => bit list"
-  "int_to_bv n == if 0 \<le> n
+  "int_to_bv n = (if 0 \<le> n
                  then norm_signed (\<zero>#nat_to_bv (nat n))
-                 else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
+                 else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))"
 
 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))"
   by (simp add: int_to_bv_def)
@@ -1003,9 +1003,11 @@
   qed
 qed
 
-constdefs
+definition
   bv_to_int :: "bit list => int"
-  "bv_to_int w == case bv_msb w of \<zero> => int (bv_to_nat w) | \<one> => - int (bv_to_nat (bv_not w) + 1)"
+  "bv_to_int w =
+    (case bv_msb w of \<zero> => int (bv_to_nat w)
+    | \<one> => - int (bv_to_nat (bv_not w) + 1))"
 
 lemma bv_to_int_Nil [simp]: "bv_to_int [] = 0"
   by (simp add: bv_to_int_def)
@@ -1232,23 +1234,23 @@
       assume "norm_unsigned w' = []"
       with weq and w0
       show False
-	by (simp add: norm_empty_bv_to_nat_zero)
+        by (simp add: norm_empty_bv_to_nat_zero)
     next
       assume w'0: "norm_unsigned w' \<noteq> []"
       have "0 < bv_to_nat w'"
       proof (rule ccontr)
-	assume "~ (0 < bv_to_nat w')"
-	hence "bv_to_nat w' = 0"
-	  by arith
-	hence "norm_unsigned w' = []"
-	  by (simp add: bv_to_nat_zero_imp_empty)
-	with w'0
-	show False
-	  by simp
+        assume "~ (0 < bv_to_nat w')"
+        hence "bv_to_nat w' = 0"
+          by arith
+        hence "norm_unsigned w' = []"
+          by (simp add: bv_to_nat_zero_imp_empty)
+        with w'0
+        show False
+          by simp
       qed
       with bv_to_nat_lower_limit [of w']
       show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')"
-	by (simp add: int_nat_two_exp)
+        by (simp add: int_nat_two_exp)
     qed
   next
     fix w'
@@ -1327,47 +1329,47 @@
     proof (rule bit_list_cases [of "norm_signed w"])
       assume "norm_signed w = []"
       hence "bv_to_int (norm_signed w) = 0"
-	by simp
+        by simp
       with w0
       show ?thesis
-	by simp
+        by simp
     next
       fix w'
       assume nw: "norm_signed w = \<zero> # w'"
       from msbw
       have "bv_msb (norm_signed w) = \<one>"
-	by simp
+        by simp
       with nw
       show ?thesis
-	by simp
+        by simp
     next
       fix w'
       assume weq: "norm_signed w = \<one> # w'"
       show ?thesis
       proof (rule bit_list_cases [of w'])
-	assume w'eq: "w' = []"
-	from w0
-	have "bv_to_int (norm_signed w) < -1"
-	  by simp
-	with w'eq and weq
-	show ?thesis
-	  by simp
+        assume w'eq: "w' = []"
+        from w0
+        have "bv_to_int (norm_signed w) < -1"
+          by simp
+        with w'eq and weq
+        show ?thesis
+          by simp
       next
-	fix w''
-	assume w'eq: "w' = \<zero> # w''"
-	show ?thesis
-	  apply (simp add: weq w'eq)
-	  apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
-	  apply (simp add: int_nat_two_exp)
-	  apply (rule add_le_less_mono)
-	  apply simp_all
-	  done
+        fix w''
+        assume w'eq: "w' = \<zero> # w''"
+        show ?thesis
+          apply (simp add: weq w'eq)
+          apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
+          apply (simp add: int_nat_two_exp)
+          apply (rule add_le_less_mono)
+          apply simp_all
+          done
       next
-	fix w''
-	assume w'eq: "w' = \<one> # w''"
-	with weq and msb_tl
-	show ?thesis
-	  by simp
+        fix w''
+        assume w'eq: "w' = \<one> # w''"
+        with weq and msb_tl
+        show ?thesis
+          by simp
       qed
     qed
   qed
@@ -1396,7 +1398,7 @@
     proof (rule bv_to_int_lower_limit_gt0)
       from w0
       show "0 < bv_to_int (int_to_bv i)"
-	by simp
+        by simp
     qed
     thus ?thesis
       by simp
@@ -1586,9 +1588,9 @@
 
 subsubsection {* Conversion from unsigned to signed *}
 
-constdefs
+definition
   utos :: "bit list => bit list"
-  "utos w == norm_signed (\<zero> # w)"
+  "utos w = norm_signed (\<zero> # w)"
 
 lemma utos_type [simp]: "utos (norm_unsigned w) = utos w"
   by (simp add: utos_def norm_signed_Cons)
@@ -1610,9 +1612,9 @@
 
 subsubsection {* Unary minus *}
 
-constdefs
+definition
   bv_uminus :: "bit list => bit list"
-  "bv_uminus w == int_to_bv (- bv_to_int w)"
+  "bv_uminus w = int_to_bv (- bv_to_int w)"
 
 lemma bv_uminus_type [simp]: "bv_uminus (norm_signed w) = bv_uminus w"
   by (simp add: bv_uminus_def)
@@ -1636,16 +1638,16 @@
     proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
       from prems
       show "bv_to_int w < 0"
-	by simp
+        by simp
     next
       have "-(2^(length w - 1)) \<le> bv_to_int w"
-	by (rule bv_to_int_lower_range)
+        by (rule bv_to_int_lower_range)
       hence "- bv_to_int w \<le> 2^(length w - 1)"
-	by simp
+        by simp
       also from lw have "... < 2 ^ length w"
-	by simp
+        by simp
       finally show "- bv_to_int w < 2 ^ length w"
-	by simp
+        by simp
     qed
   next
     assume p: "- bv_to_int w = 1"
@@ -1674,10 +1676,10 @@
       apply simp
     proof -
       have "bv_to_int w < 2 ^ (length w - 1)"
-	by (rule bv_to_int_upper_range)
+        by (rule bv_to_int_upper_range)
       also have "... \<le> 2 ^ length w" by simp
       finally show "bv_to_int w \<le> 2 ^ length w"
-	by simp
+        by simp
     qed
   qed
 qed
@@ -1709,9 +1711,9 @@
   qed
 qed
 
-constdefs
+definition
   bv_sadd :: "[bit list, bit list ] => bit list"
-  "bv_sadd w1 w2 == int_to_bv (bv_to_int w1 + bv_to_int w2)"
+  "bv_sadd w1 w2 = int_to_bv (bv_to_int w1 + bv_to_int w2)"
 
 lemma bv_sadd_type1 [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2"
   by (simp add: bv_sadd_def)
@@ -1756,10 +1758,10 @@
       assume [simp]: "w1 = []"
       show "w2 \<noteq> []"
       proof (rule ccontr,simp)
-	assume [simp]: "w2 = []"
-	from p
-	show False
-	  by simp
+        assume [simp]: "w2 = []"
+        from p
+        show False
+          by simp
       qed
     qed
   qed
@@ -1784,18 +1786,18 @@
     proof simp
       from bv_to_int_upper_range [of w2]
       have "bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
-	by simp
+        by simp
       with bv_to_int_upper_range [of w1]
       have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
-	by (rule zadd_zless_mono)
+        by (rule zadd_zless_mono)
       also have "... \<le> 2 ^ max (length w1) (length w2)"
-	apply (rule adder_helper)
-	apply (rule helper)
-	using p
-	apply simp
-	done
+        apply (rule adder_helper)
+        apply (rule helper)
+        using p
+        apply simp
+        done
       finally show "?Q < 2 ^ max (length w1) (length w2)"
-	.
+        .
     qed
   next
     assume p: "?Q < -1"
@@ -1805,26 +1807,26 @@
       apply (rule p)
     proof -
       have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
-	apply (rule adder_helper)
-	apply (rule helper)
-	using p
-	apply simp
-	done
+        apply (rule adder_helper)
+        apply (rule helper)
+        using p
+        apply simp
+        done
       hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
-	by simp
+        by simp
       also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?Q"
-	apply (rule add_mono)
-	apply (rule bv_to_int_lower_range [of w1])
-	apply (rule bv_to_int_lower_range [of w2])
-	done
+        apply (rule add_mono)
+        apply (rule bv_to_int_lower_range [of w1])
+        apply (rule bv_to_int_lower_range [of w2])
+        done
       finally show "- (2^max (length w1) (length w2)) \<le> ?Q" .
     qed
   qed
 qed
 
-constdefs
+definition
   bv_sub :: "[bit list, bit list] => bit list"
-  "bv_sub w1 w2 == bv_sadd w1 (bv_uminus w2)"
+  "bv_sub w1 w2 = bv_sadd w1 (bv_uminus w2)"
 
 lemma bv_sub_type1 [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2"
   by (simp add: bv_sub_def)
@@ -1878,18 +1880,18 @@
     proof simp
       from bv_to_int_lower_range [of w2]
       have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
-	by simp
+        by simp
       have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
-	apply (rule zadd_zless_mono)
-	apply (rule bv_to_int_upper_range [of w1])
-	apply (rule v2)
-	done
+        apply (rule zadd_zless_mono)
+        apply (rule bv_to_int_upper_range [of w1])
+        apply (rule v2)
+        done
       also have "... \<le> 2 ^ max (length w1) (length w2)"
-	apply (rule adder_helper)
-	apply (rule lmw)
-	done
+        apply (rule adder_helper)
+        apply (rule lmw)
+        done
       finally show "?Q < 2 ^ max (length w1) (length w2)"
-	by simp
+        by simp
     qed
   next
     assume p: "?Q < -1"
@@ -1899,26 +1901,26 @@
       apply (rule p)
     proof simp
       have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
-	apply (rule adder_helper)
-	apply (rule lmw)
-	done
+        apply (rule adder_helper)
+        apply (rule lmw)
+        done
       hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
-	by simp
+        by simp
       also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2"
-	apply (rule add_mono)
-	apply (rule bv_to_int_lower_range [of w1])
-	using bv_to_int_upper_range [of w2]
-	apply simp
-	done
+        apply (rule add_mono)
+        apply (rule bv_to_int_lower_range [of w1])
+        using bv_to_int_upper_range [of w2]
+        apply simp
+        done
       finally show "- (2^max (length w1) (length w2)) \<le> ?Q"
-	by simp
+        by simp
     qed
   qed
 qed
 
-constdefs
+definition
   bv_smult :: "[bit list, bit list] => bit list"
-  "bv_smult w1 w2 == int_to_bv (bv_to_int w1 * bv_to_int w2)"
+  "bv_smult w1 w2 = int_to_bv (bv_to_int w1 * bv_to_int w2)"
 
 lemma bv_smult_type1 [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"
   by (simp add: bv_smult_def)
@@ -1963,58 +1965,58 @@
       assume bi1: "0 < bv_to_int w1"
       assume bi2: "0 < bv_to_int w2"
       show ?thesis
-	apply (simp add: bv_smult_def)
-	apply (rule length_int_to_bv_upper_limit_gt0)
-	apply (rule p)
+        apply (simp add: bv_smult_def)
+        apply (rule length_int_to_bv_upper_limit_gt0)
+        apply (rule p)
       proof simp
-	have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
-	  apply (rule mult_strict_mono)
-	  apply (rule bv_to_int_upper_range)
-	  apply (rule bv_to_int_upper_range)
-	  apply (rule zero_less_power)
-	  apply simp
-	  using bi2
-	  apply simp
-	  done
-	also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
-	  apply simp
-	  apply (subst zpower_zadd_distrib [symmetric])
-	  apply simp
-	  apply arith
-	  done
-	finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
-	  .
+        have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
+          apply (rule mult_strict_mono)
+          apply (rule bv_to_int_upper_range)
+          apply (rule bv_to_int_upper_range)
+          apply (rule zero_less_power)
+          apply simp
+          using bi2
+          apply simp
+          done
+        also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
+          apply simp
+          apply (subst zpower_zadd_distrib [symmetric])
+          apply simp
+          apply arith
+          done
+        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
+          .
       qed
     next
       assume bi1: "bv_to_int w1 < 0"
       assume bi2: "bv_to_int w2 < 0"
       show ?thesis
-	apply (simp add: bv_smult_def)
-	apply (rule length_int_to_bv_upper_limit_gt0)
-	apply (rule p)
+        apply (simp add: bv_smult_def)
+        apply (rule length_int_to_bv_upper_limit_gt0)
+        apply (rule p)
       proof simp
-	have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
-	  apply (rule mult_mono)
-	  using bv_to_int_lower_range [of w1]
-	  apply simp
-	  using bv_to_int_lower_range [of w2]
-	  apply simp
-	  apply (rule zero_le_power,simp)
-	  using bi2
-	  apply simp
-	  done
-	hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
-	  by simp
-	also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
-	  apply simp
-	  apply (subst zpower_zadd_distrib [symmetric])
-	  apply simp
-	  apply (cut_tac lmw)
-	  apply arith
-	  apply (cut_tac p)
-	  apply arith
-	  done
-	finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
+        have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
+          apply (rule mult_mono)
+          using bv_to_int_lower_range [of w1]
+          apply simp
+          using bv_to_int_lower_range [of w2]
+          apply simp
+          apply (rule zero_le_power,simp)
+          using bi2
+          apply simp
+          done
+        hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
+          by simp
+        also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
+          apply simp
+          apply (subst zpower_zadd_distrib [symmetric])
+          apply simp
+          apply (cut_tac lmw)
+          apply arith
+          apply (cut_tac p)
+          apply arith
+          done
+        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
       qed
     qed
   next
@@ -2025,60 +2027,60 @@
       apply (rule p)
     proof simp
       have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
-	apply simp
-	apply (subst zpower_zadd_distrib [symmetric])
-	apply simp
-	apply (cut_tac lmw)
-	apply arith
-	apply (cut_tac p)
-	apply arith
-	done
+        apply simp
+        apply (subst zpower_zadd_distrib [symmetric])
+        apply simp
+        apply (cut_tac lmw)
+        apply arith
+        apply (cut_tac p)
+        apply arith
+        done
       hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
-	by simp
+        by simp
       also have "... \<le> ?Q"
       proof -
-	from p
-	have q: "bv_to_int w1 * bv_to_int w2 < 0"
-	  by simp
-	thus ?thesis
-	proof (simp add: mult_less_0_iff,safe)
-	  assume bi1: "0 < bv_to_int w1"
-	  assume bi2: "bv_to_int w2 < 0"
-	  have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
-	    apply (rule mult_mono)
-	    using bv_to_int_lower_range [of w2]
-	    apply simp
-	    using bv_to_int_upper_range [of w1]
-	    apply simp
-	    apply (rule zero_le_power,simp)
-	    using bi1
-	    apply simp
-	    done
-	  hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
-	    by (simp add: zmult_ac)
-	  thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
-	    by simp
-	next
-	  assume bi1: "bv_to_int w1 < 0"
-	  assume bi2: "0 < bv_to_int w2"
-	  have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
-	    apply (rule mult_mono)
-	    using bv_to_int_lower_range [of w1]
-	    apply simp
-	    using bv_to_int_upper_range [of w2]
-	    apply simp
-	    apply (rule zero_le_power,simp)
-	    using bi2
-	    apply simp
-	    done
-	  hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
-	    by (simp add: zmult_ac)
-	  thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
-	    by simp
-	qed
+        from p
+        have q: "bv_to_int w1 * bv_to_int w2 < 0"
+          by simp
+        thus ?thesis
+        proof (simp add: mult_less_0_iff,safe)
+          assume bi1: "0 < bv_to_int w1"
+          assume bi2: "bv_to_int w2 < 0"
+          have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
+            apply (rule mult_mono)
+            using bv_to_int_lower_range [of w2]
+            apply simp
+            using bv_to_int_upper_range [of w1]
+            apply simp
+            apply (rule zero_le_power,simp)
+            using bi1
+            apply simp
+            done
+          hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
+            by (simp add: zmult_ac)
+          thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
+            by simp
+        next
+          assume bi1: "bv_to_int w1 < 0"
+          assume bi2: "0 < bv_to_int w2"
+          have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
+            apply (rule mult_mono)
+            using bv_to_int_lower_range [of w1]
+            apply simp
+            using bv_to_int_upper_range [of w2]
+            apply simp
+            apply (rule zero_le_power,simp)
+            using bi2
+            apply simp
+            done
+          hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
+            by (simp add: zmult_ac)
+          thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
+            by simp
+        qed
       qed
       finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
-	.
+        .
     qed
   qed
 qed
@@ -2110,35 +2112,35 @@
     proof (simp add: zero_less_mult_iff,safe)
       assume biw2: "0 < bv_to_int w2"
       show ?thesis
-	apply (simp add: bv_smult_def)
-	apply (rule length_int_to_bv_upper_limit_gt0)
-	apply (rule p)
+        apply (simp add: bv_smult_def)
+        apply (rule length_int_to_bv_upper_limit_gt0)
+        apply (rule p)
       proof simp
-	have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
-	  apply (rule mult_strict_mono)
-	  apply (simp add: bv_to_int_utos int_nat_two_exp)
-	  apply (rule bv_to_nat_upper_range)
-	  apply (rule bv_to_int_upper_range)
-	  apply (rule zero_less_power,simp)
-	  using biw2
-	  apply simp
-	  done
-	also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- 	  apply simp
-	  apply (subst zpower_zadd_distrib [symmetric])
-	  apply simp
-	  apply (cut_tac lmw)
-	  apply arith
-	  using p
-	  apply auto
-	  done
-	finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
-	  .
+        have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
+          apply (rule mult_strict_mono)
+          apply (simp add: bv_to_int_utos int_nat_two_exp)
+          apply (rule bv_to_nat_upper_range)
+          apply (rule bv_to_int_upper_range)
+          apply (rule zero_less_power,simp)
+          using biw2
+          apply simp
+          done
+        also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
+          apply simp
+          apply (subst zpower_zadd_distrib [symmetric])
+          apply simp
+          apply (cut_tac lmw)
+          apply arith
+          using p
+          apply auto
+          done
+        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
+          .
       qed
     next
       assume "bv_to_int (utos w1) < 0"
       thus ?thesis
-	by (simp add: bv_to_int_utos)
+        by (simp add: bv_to_int_utos)
     qed
   next
     assume p: "?Q = -1"
@@ -2156,48 +2158,48 @@
       apply (rule p)
     proof simp
       have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
-	apply simp
-	apply (subst zpower_zadd_distrib [symmetric])
-	apply simp
-	apply (cut_tac lmw)
-	apply arith
-	apply (cut_tac p)
-	apply arith
-	done
+        apply simp
+        apply (subst zpower_zadd_distrib [symmetric])
+        apply simp
+        apply (cut_tac lmw)
+        apply arith
+        apply (cut_tac p)
+        apply arith
+        done
       hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))"
-	by simp
+        by simp
       also have "... \<le> ?Q"
       proof -
-	from p
-	have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
-	  by simp
-	thus ?thesis
-	proof (simp add: mult_less_0_iff,safe)
-	  assume bi1: "0 < bv_to_int (utos w1)"
-	  assume bi2: "bv_to_int w2 < 0"
-	  have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
-	    apply (rule mult_mono)
-	    using bv_to_int_lower_range [of w2]
-	    apply simp
-	    apply (simp add: bv_to_int_utos)
-	    using bv_to_nat_upper_range [of w1]
-	    apply (simp add: int_nat_two_exp)
-	    apply (rule zero_le_power,simp)
-	    using bi1
-	    apply simp
-	    done
-	  hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
-	    by (simp add: zmult_ac)
-	  thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
-	    by simp
-	next
-	  assume bi1: "bv_to_int (utos w1) < 0"
-	  thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
-	    by (simp add: bv_to_int_utos)
-	qed
+        from p
+        have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
+          by simp
+        thus ?thesis
+        proof (simp add: mult_less_0_iff,safe)
+          assume bi1: "0 < bv_to_int (utos w1)"
+          assume bi2: "bv_to_int w2 < 0"
+          have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
+            apply (rule mult_mono)
+            using bv_to_int_lower_range [of w2]
+            apply simp
+            apply (simp add: bv_to_int_utos)
+            using bv_to_nat_upper_range [of w1]
+            apply (simp add: int_nat_two_exp)
+            apply (rule zero_le_power,simp)
+            using bi1
+            apply simp
+            done
+          hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
+            by (simp add: zmult_ac)
+          thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
+            by simp
+        next
+          assume bi1: "bv_to_int (utos w1) < 0"
+          thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
+            by (simp add: bv_to_int_utos)
+        qed
       qed
       finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
-	.
+        .
     qed
   qed
 qed
@@ -2207,13 +2209,13 @@
 
 subsection {* Structural operations *}
 
-constdefs
+definition
   bv_select :: "[bit list,nat] => bit"
-  "bv_select w i == w ! (length w - 1 - i)"
+  "bv_select w i = w ! (length w - 1 - i)"
   bv_chop :: "[bit list,nat] => bit list * bit list"
-  "bv_chop w i == let len = length w in (take (len - i) w,drop (len - i) w)"
+  "bv_chop w i = (let len = length w in (take (len - i) w,drop (len - i) w))"
   bv_slice :: "[bit list,nat*nat] => bit list"
-  "bv_slice w == \<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e)"
+  "bv_slice w = (\<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e))"
 
 lemma bv_select_rev:
   assumes notnull: "n < length w"
@@ -2230,36 +2232,36 @@
       assume "xs = []"
       with notx
       show ?thesis
-	by simp
+        by simp
     next
       fix y ys
       assume [simp]: "xs = y # ys"
       show ?thesis
       proof (auto simp add: nth_append)
-	assume noty: "n < length ys"
-	from spec [OF ind,of ys]
-	have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
-	  by simp
-	hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
-	  ..
-	hence "ys ! (length ys - Suc n) = rev ys ! n"
-	  ..
-	thus "(y # ys) ! (length ys - n) = rev ys ! n"
-	  by (simp add: nth_Cons' noty linorder_not_less [symmetric])
+        assume noty: "n < length ys"
+        from spec [OF ind,of ys]
+        have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
+          by simp
+        hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
+          ..
+        hence "ys ! (length ys - Suc n) = rev ys ! n"
+          ..
+        thus "(y # ys) ! (length ys - n) = rev ys ! n"
+          by (simp add: nth_Cons' noty linorder_not_less [symmetric])
       next
-	assume "~ n < length ys"
-	hence x: "length ys \<le> n"
-	  by simp
-	from notx
-	have "n < Suc (length ys)"
-	  by simp
-	hence "n \<le> length ys"
-	  by simp
-	with x
-	have "length ys = n"
-	  by simp
-	thus "y = [y] ! (n - length ys)"
-	  by simp
+        assume "~ n < length ys"
+        hence x: "length ys \<le> n"
+          by simp
+        from notx
+        have "n < Suc (length ys)"
+          by simp
+        hence "n \<le> length ys"
+          by simp
+        with x
+        have "length ys = n"
+          by simp
+        thus "y = [y] ! (n - length ys)"
+          by simp
       qed
     qed
   qed
@@ -2284,9 +2286,9 @@
 lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
   by (auto simp add: bv_slice_def,arith)
 
-constdefs
+definition
   length_nat :: "nat => nat"
-  "length_nat x == LEAST n. x < 2 ^ n"
+  "length_nat x = (LEAST n. x < 2 ^ n)"
 
 lemma length_nat: "length (nat_to_bv n) = length_nat n"
   apply (simp add: length_nat_def)
@@ -2316,9 +2318,12 @@
   apply (simp_all add: n0)
   done
 
-constdefs
+definition
   length_int :: "int => nat"
-  "length_int x == if 0 < x then Suc (length_nat (nat x)) else if x = 0 then 0 else Suc (length_nat (nat (-x - 1)))"
+  "length_int x =
+    (if 0 < x then Suc (length_nat (nat x))
+    else if x = 0 then 0
+    else Suc (length_nat (nat (-x - 1))))"
 
 lemma length_int: "length (int_to_bv i) = length_int i"
 proof (cases "0 < i")
@@ -2410,12 +2415,11 @@
   shows       "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
 proof -
   def w1  == "fst (bv_chop w (Suc l))"
-  def w2  == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
-  def w3  == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
-  def w4  == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
-  def w5  == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
-
-  note w_defs = w1_def w2_def w3_def w4_def w5_def
+  and w2  == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
+  and w3  == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
+  and w4  == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
+  and w5  == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
+  note w_defs = this
 
   have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"
     by (simp add: w_defs append_bv_chop_id)
@@ -2443,12 +2447,14 @@
   apply (simp add: bv_extend_def)
   apply (subst bv_to_nat_dist_append)
   apply simp
-  apply (induct "n - length w",simp_all)
+  apply (induct "n - length w")
+   apply simp_all
   done
 
 lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
   apply (simp add: bv_extend_def)
-  apply (induct "n - length w",simp_all)
+  apply (induct "n - length w")
+   apply simp_all
   done
 
 lemma bv_to_int_extend [simp]:
@@ -2632,18 +2638,21 @@
 declare bv_to_nat1 [simp del]
 declare bv_to_nat_helper [simp del]
 
-constdefs
+definition
   bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list"
-  "bv_mapzip f w1 w2 == let g = bv_extend (max (length w1) (length w2)) \<zero>
-                        in map (split f) (zip (g w1) (g w2))"
+  "bv_mapzip f w1 w2 =
+    (let g = bv_extend (max (length w1) (length w2)) \<zero>
+     in map (split f) (zip (g w1) (g w2)))"
 
-lemma bv_length_bv_mapzip [simp]: "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
+lemma bv_length_bv_mapzip [simp]:
+  "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
   by (simp add: bv_mapzip_def Let_def split: split_max)
 
 lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"
   by (simp add: bv_mapzip_def Let_def)
 
-lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==> bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
+lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==>
+    bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
   by (simp add: bv_mapzip_def Let_def)
 
 end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Zorn.thy	Sat May 27 17:42:02 2006 +0200
@@ -15,24 +15,23 @@
   \cite{Abrial-Laffitte}.
 *}
 
-constdefs
+definition
   chain     ::  "'a set set => 'a set set set"
-  "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
+  "chain S  = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
 
   super     ::  "['a set set,'a set set] => 'a set set set"
-  "super S c == {d. d \<in> chain S & c \<subset> d}"
+  "super S c = {d. d \<in> chain S & c \<subset> d}"
 
   maxchain  ::  "'a set set => 'a set set set"
-  "maxchain S == {c. c \<in> chain S & super S c = {}}"
+  "maxchain S = {c. c \<in> chain S & super S c = {}}"
 
   succ      ::  "['a set set,'a set set] => 'a set set"
-  "succ S c ==
-    if c \<notin> chain S | c \<in> maxchain S
-    then c else SOME c'. c' \<in> super S c"
+  "succ S c =
+    (if c \<notin> chain S | c \<in> maxchain S
+    then c else SOME c'. c' \<in> super S c)"
 
 consts
   TFin :: "'a set set => 'a set set set"
-
 inductive "TFin S"
   intros
     succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
@@ -64,7 +63,7 @@
              !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
              !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
           ==> P(n)"
-  apply (erule TFin.induct)
+  apply (induct set: TFin)
    apply blast+
   done
 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Sat May 27 17:42:02 2006 +0200
@@ -14,12 +14,12 @@
 
 lemmas [elim?] = lub.least lub.upper
 
-constdefs
+definition
   the_lub :: "'a::order set \<Rightarrow> 'a"
-  "the_lub A \<equiv> The (lub A)"
+  "the_lub A = The (lub A)"
 
-syntax (xsymbols)
-  the_lub :: "'a::order set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
+const_syntax (xsymbols)
+  the_lub  ("\<Squnion>_" [90] 90)
 
 lemma the_lub_equality [elim?]:
   includes lub
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sat May 27 17:42:02 2006 +0200
@@ -22,9 +22,9 @@
 
 types 'a graph = "('a \<times> real) set"
 
-constdefs
+definition
   graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph"
-  "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
+  "graph F f = {(x, f x) | x. x \<in> F}"
 
 lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
   by (unfold graph_def) blast
@@ -65,12 +65,12 @@
   funct}.
 *}
 
-constdefs
+definition
   "domain" :: "'a graph \<Rightarrow> 'a set"
-  "domain g \<equiv> {x. \<exists>y. (x, y) \<in> g}"
+  "domain g = {x. \<exists>y. (x, y) \<in> g}"
 
   funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
-  "funct g \<equiv> \<lambda>x. (SOME y. (x, y) \<in> g)"
+  "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
 
 text {*
   The following lemma states that @{text g} is the graph of a function
@@ -101,12 +101,12 @@
   @{text p}, is defined as follows.
 *}
 
-constdefs
+definition
   norm_pres_extensions ::
     "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
       \<Rightarrow> 'a graph set"
     "norm_pres_extensions E p F f
-      \<equiv> {g. \<exists>H h. g = graph H h
+      = {g. \<exists>H h. g = graph H h
           \<and> linearform H h
           \<and> H \<unlhd> E
           \<and> F \<unlhd> H
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sat May 27 17:42:02 2006 +0200
@@ -22,10 +22,10 @@
     and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
     and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
 
-declare vectorspace.intro [intro?] subspace.intro [intro?]
+const_syntax (symbols)
+  subspace  (infix "\<unlhd>" 50)
 
-syntax (symbols)
-  subspace :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"    (infix "\<unlhd>" 50)
+declare vectorspace.intro [intro?] subspace.intro [intro?]
 
 lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
   by (rule subspace.subset)
@@ -130,9 +130,9 @@
   scalar multiples of @{text x}.
 *}
 
-constdefs
+definition
   lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set"
-  "lin x \<equiv> {a \<cdot> x | a. True}"
+  "lin x = {a \<cdot> x | a. True}"
 
 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
   by (unfold lin_def) blast
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Sat May 27 17:42:02 2006 +0200
@@ -18,10 +18,10 @@
 consts
   prod  :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a"     (infixr "'(*')" 70)
 
-syntax (xsymbols)
-  prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
-syntax (HTML output)
-  prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
+const_syntax (xsymbols)
+  prod  (infixr "\<cdot>" 70)
+const_syntax (HTML output)
+  prod  (infixr "\<cdot>" 70)
 
 
 subsection {* Vector space laws *}
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/W0/W0.thy	Sat May 27 17:42:02 2006 +0200
@@ -11,9 +11,9 @@
 
 datatype 'a maybe = Ok 'a | Fail
 
-constdefs
+definition
   bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe"    (infixl "\<bind>" 60)
-  "m \<bind> f \<equiv> case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail"
+  "m \<bind> f = (case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail)"
 
 syntax
   "_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c"    ("(_ := _;//_)" 0)
@@ -84,16 +84,16 @@
   "free_tv [] = {}"
   "free_tv (x # xs) = free_tv x \<union> free_tv xs"
 
-constdefs
+definition
   dom :: "subst \<Rightarrow> nat set"
-  "dom s \<equiv> {n. s n \<noteq> TVar n}"
+  "dom s = {n. s n \<noteq> TVar n}"
   -- {* domain of a substitution *}
 
   cod :: "subst \<Rightarrow> nat set"
-  "cod s \<equiv> \<Union>m \<in> dom s. free_tv (s m)"
+  "cod s = (\<Union>m \<in> dom s. free_tv (s m))"
   -- {* codomain of a substitutions: the introduced variables *}
 
-defs
+defs (overloaded)
   free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s"
 
 text {*
@@ -102,16 +102,16 @@
   than any type variable occuring in the type structure.
 *}
 
-constdefs
+definition
   new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool"
-  "new_tv n ts \<equiv> \<forall>m. m \<in> free_tv ts \<longrightarrow> m < n"
+  "new_tv n ts = (\<forall>m. m \<in> free_tv ts \<longrightarrow> m < n)"
 
 
 subsubsection {* Identity substitution *}
 
-constdefs
+definition
   id_subst :: subst
-  "id_subst \<equiv> \<lambda>n. TVar n"
+  "id_subst = (\<lambda>n. TVar n)"
 
 lemma app_subst_id_te [simp]:
   "$id_subst = (\<lambda>t::typ. t)"
@@ -218,35 +218,36 @@
   by (induct x) simp_all
 
 lemma subst_te_new_tv [simp]:
-  "new_tv n (t::typ) \<longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
+  "new_tv n (t::typ) \<Longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
   -- {* substitution affects only variables occurring freely *}
   by (induct t) simp_all
 
 lemma subst_tel_new_tv [simp]:
-  "new_tv n (ts::typ list) \<longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
+  "new_tv n (ts::typ list) \<Longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
   by (induct ts) simp_all
 
 lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
   -- {* all greater variables are also new *}
 proof (induct t)
   case (TVar n)
-  thus ?case by (auto intro: less_le_trans)
+  then show ?case by (auto intro: less_le_trans)
 next
   case TFun
-  thus ?case by simp
+  then show ?case by simp
 qed
 
 lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
   by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
 
 lemma new_tv_list_le:
-  "n \<le> m \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
+  assumes "n \<le> m"
+  shows "new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
 proof (induct ts)
   case Nil
-  thus ?case by simp
+  then show ?case by simp
 next
   case Cons
-  thus ?case by (auto intro: new_tv_le)
+  with `n \<le> m` show ?case by (auto intro: new_tv_le)
 qed
 
 lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
@@ -397,31 +398,27 @@
 text {* Type assigment is closed wrt.\ substitution. *}
 
 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
-proof -
-  assume "a |- e :: t"
-  thus ?thesis (is "?P a e t")
-  proof induct
-    case (Var a n)
-    hence "n < length (map ($ s) a)" by simp
-    hence "map ($ s) a |- Var n :: map ($ s) a ! n"
-      by (rule has_type.Var)
-    also have "map ($ s) a ! n = $ s (a ! n)"
-      by (rule nth_map)
-    also have "map ($ s) a = $ s a"
-      by (simp only: app_subst_list)
-    finally show "?P a (Var n) (a ! n)" .
-  next
-    case (Abs a e t1 t2)
-    hence "$ s t1 # map ($ s) a |- e :: $ s t2"
-      by (simp add: app_subst_list)
-    hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
-      by (rule has_type.Abs)
-    thus "?P a (Abs e) (t1 -> t2)"
-      by (simp add: app_subst_list)
-  next
-    case App
-    thus ?case by (simp add: has_type.App)
-  qed
+proof (induct set: has_type)
+  case (Var a n)
+  then have "n < length (map ($ s) a)" by simp
+  then have "map ($ s) a |- Var n :: map ($ s) a ! n"
+    by (rule has_type.Var)
+  also have "map ($ s) a ! n = $ s (a ! n)"
+    by (rule nth_map)
+  also have "map ($ s) a = $ s a"
+    by (simp only: app_subst_list)
+  finally show ?case .
+next
+  case (Abs a e t1 t2)
+  then have "$ s t1 # map ($ s) a |- e :: $ s t2"
+    by (simp add: app_subst_list)
+  then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
+    by (rule has_type.Abs)
+  then show ?case
+    by (simp add: app_subst_list)
+next
+  case App
+  then show ?case by (simp add: has_type.App)
 qed
 
 
@@ -442,52 +439,48 @@
      u := mgu ($ s2 t1) (t2 -> TVar m2);
      Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
 
-theorem W_correct: "!!a s t m n. Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
-  (is "PROP ?P e")
-proof (induct e)
-  fix a s t m n
-  {
-    fix i
-    assume "Ok (s, t, m) = \<W> (Var i) a n"
-    thus "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
-  next
-    fix e assume hyp: "PROP ?P e"
-    assume "Ok (s, t, m) = \<W> (Abs e) a n"
-    then obtain t' where "t = s n -> t'"
-        and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
-      by (auto split: bind_splits)
-    with hyp show "$s a |- Abs e :: t"
-      by (force intro: has_type.Abs)
-  next
-    fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
-    assume "Ok (s, t, m) = \<W> (App e1 e2) a n"
-    then obtain s1 t1 n1 s2 t2 n2 u where
+theorem W_correct: "Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
+proof (induct e fixing: a s t m n)
+  case (Var i)
+  from `Ok (s, t, m) = \<W> (Var i) a n`
+  show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
+next
+  case (Abs e)
+  from `Ok (s, t, m) = \<W> (Abs e) a n`
+  obtain t' where "t = s n -> t'"
+      and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
+    by (auto split: bind_splits)
+  with Abs.hyps show "$s a |- Abs e :: t"
+    by (force intro: has_type.Abs)
+next
+  case (App e1 e2)
+  from `Ok (s, t, m) = \<W> (App e1 e2) a n`
+  obtain s1 t1 n1 s2 t2 n2 u where
           s: "s = $u o $s2 o s1"
-        and t: "t = u n2"
-        and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
-        and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
-        and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
-      by (auto split: bind_splits simp: that)
-    show "$s a |- App e1 e2 :: t"
-    proof (rule has_type.App)
-      from s have s': "$u ($s2 ($s1 a)) = $s a"
-        by (simp add: subst_comp_tel o_def)
-      show "$s a |- e1 :: $u t2 -> t"
-      proof -
-        from W1_ok have "$s1 a |- e1 :: t1" by (rule hyp1)
-        hence "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
-          by (intro has_type_subst_closed)
-        with s' t mgu_ok show ?thesis by simp
-      qed
-      show "$s a |- e2 :: $u t2"
-      proof -
-        from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule hyp2)
-        hence "$u ($s2 ($s1 a)) |- e2 :: $u t2"
-          by (rule has_type_subst_closed)
-        with s' show ?thesis by simp
-      qed
+      and t: "t = u n2"
+      and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
+      and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
+      and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
+    by (auto split: bind_splits simp: that)
+  show "$s a |- App e1 e2 :: t"
+  proof (rule has_type.App)
+    from s have s': "$u ($s2 ($s1 a)) = $s a"
+      by (simp add: subst_comp_tel o_def)
+    show "$s a |- e1 :: $u t2 -> t"
+    proof -
+      from W1_ok have "$s1 a |- e1 :: t1" by (rule App.hyps)
+      then have "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
+        by (intro has_type_subst_closed)
+      with s' t mgu_ok show ?thesis by simp
     qed
-  }
+    show "$s a |- e2 :: $u t2"
+    proof -
+      from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule App.hyps)
+      then have "$u ($s2 ($s1 a)) |- e2 :: $u t2"
+        by (rule has_type_subst_closed)
+      with s' show ?thesis by simp
+    qed
+  qed
 qed
 
 
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Adder.thy
--- a/src/HOL/ex/Adder.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Adder.thy	Sat May 27 17:42:02 2006 +0200
@@ -13,9 +13,9 @@
 lemma bv_to_nat_helper': "bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)"
   by (cases bv,simp_all add: bv_to_nat_helper)
 
-constdefs
+definition
   half_adder :: "[bit,bit] => bit list"
-  "half_adder a b == [a bitand b,a bitxor b]"
+  "half_adder a b = [a bitand b,a bitxor b]"
 
 lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b"
   apply (simp add: half_adder_def)
@@ -26,10 +26,10 @@
 lemma [simp]: "length (half_adder a b) = 2"
   by (simp add: half_adder_def)
 
-constdefs
+definition
   full_adder :: "[bit,bit,bit] => bit list"
-  "full_adder a b c == 
-      let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c]"
+  "full_adder a b c =
+      (let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c])"
 
 lemma full_adder_correct:
      "bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c"
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy	Sat May 27 17:42:02 2006 +0200
@@ -13,23 +13,23 @@
 section {* Very basic *}
 
 consts fib :: "nat \<Rightarrow> nat"
-function 
+function
   "fib 0 = 1"
   "fib (Suc 0) = 1"
   "fib (Suc (Suc n)) = fib n + fib (Suc n)"
-by pat_completeness (* shows that the patterns are complete *)
-  auto (* shows that the patterns are compatible *)
+by pat_completeness  -- {* shows that the patterns are complete *}
+  auto  -- {* shows that the patterns are compatible *}
 
-(* we get partial simp and induction rules: *)
+text {* we get partial simp and induction rules: *}
 thm fib.psimps
 thm fib.pinduct
 
-(* There is also a cases rule to distinguish cases along the definition *)
+text {* There is also a cases rule to distinguish cases along the definition *}
 thm fib.cases
 
-(* Now termination: *)
+text {* Now termination: *}
 termination fib
-  by (auto_term "less_than")    
+  by (auto_term "less_than")
 
 thm fib.simps
 thm fib.induct
@@ -37,15 +37,15 @@
 
 section {* Currying *}
 
-consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
+consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 function
   "add 0 y = y"
   "add (Suc x) y = Suc (add x y)"
 by pat_completeness auto
-termination 
+termination
   by (auto_term "measure fst")
 
-thm add.induct (* Note the curried induction predicate *)
+thm add.induct -- {* Note the curried induction predicate *}
 
 
 section {* Nested recursion *}
@@ -57,14 +57,14 @@
   "nz (Suc x) = nz (nz x)"
 by pat_completeness auto
 
-lemma nz_is_zero: (* A lemma we need to prove termination *)
+lemma nz_is_zero: -- {* A lemma we need to prove termination *}
   assumes trm: "x \<in> nz_dom"
   shows "nz x = 0"
 using trm
 by induct auto
 
 termination nz
-  apply (auto_term "less_than") (* Oops, it left us something to prove *)
+  apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
   by (auto simp:nz_is_zero)
 
 thm nz.simps
@@ -73,13 +73,12 @@
 
 section {* More general patterns *}
 
-(* Currently, patterns must always be compatible with each other, since
+text {* Currently, patterns must always be compatible with each other, since
 no automatich splitting takes place. But the following definition of
-gcd is ok, although patterns overlap: *)
-
+gcd is ok, although patterns overlap: *}
 
 consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-function 
+function
   "gcd2 x 0 = x"
   "gcd2 0 y = y"
   "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
@@ -91,17 +90,17 @@
 thm gcd2.induct
 
 
-(* General patterns allow even strange definitions: *)
+text {* General patterns allow even strange definitions: *}
 consts ev :: "nat \<Rightarrow> bool"
-function 
+function
   "ev (2 * n) = True"
   "ev (2 * n + 1) = False"
-proof - (* completeness is more difficult here. . . *)
+proof -  -- {* completeness is more difficult here \dots *}
   assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
     and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
   have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
   show "P"
-  proof cases 
+  proof cases
     assume "x mod 2 = 0"
     with divmod have "x = 2 * (x div 2)" by simp
     with c1 show "P" .
@@ -111,15 +110,11 @@
     with divmod have "x = 2 * (x div 2) + 1" by simp
     with c2 show "P" .
   qed
-qed presburger+ (* solve compatibility with presburger *)
+qed presburger+   -- {* solve compatibility with presburger *}
 termination by (auto_term "{}")
 
 thm ev.simps
 thm ev.induct
 thm ev.cases
 
-
-
-
-
-end
\ No newline at end of file
+end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Sat May 27 17:42:02 2006 +0200
@@ -79,7 +79,7 @@
 
 subsubsection {* Derived connectives *}
 
-constdefs
+definition
   false :: o    ("\<bottom>")
   "\<bottom> \<equiv> \<forall>A. A"
   true :: o    ("\<top>")
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/InductiveInvariant.thy
--- a/src/HOL/ex/InductiveInvariant.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/InductiveInvariant.thy	Sat May 27 17:42:02 2006 +0200
@@ -14,14 +14,16 @@
 
 text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
 
-constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
-         "indinv r S F == \<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x)"
+definition
+  indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
+  "indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))"
 
 
 text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
 
-constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
-         "indinv_on r D S F == \<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> r --> S y (f y)) --> S x (F f x)"
+definition
+  indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
+  "indinv_on r D S F = (\<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> r --> S y (f y)) --> S x (F f x))"
 
 
 text "The key theorem, corresponding to theorem 1 of the paper. All other results
@@ -29,15 +31,16 @@
       derived from this theorem."
 
 theorem indinv_wfrec:
-  assumes WF:  "wf r" and
-          INV: "indinv r S F"
+  assumes wf:  "wf r" and
+          inv: "indinv r S F"
   shows        "S x (wfrec r F x)"
-proof (induct_tac x rule: wf_induct [OF WF])
+  using wf
+proof (induct x)
   fix x
-  assume  IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"
-  then have     "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
-  with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
-  thus "S x (wfrec r F x)" using WF by (simp add: wfrec)
+  assume  IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)"
+  then have     "!!y. (y,x) \<in> r \<Longrightarrow> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
+  with inv have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
+  thus "S x (wfrec r F x)" using wf by (simp add: wfrec)
 qed
 
 theorem indinv_on_wfrec:
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Lagrange.thy
--- a/src/HOL/ex/Lagrange.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Lagrange.thy	Sat May 27 17:42:02 2006 +0200
@@ -16,8 +16,9 @@
 The enterprising reader might consider proving all of Lagrange's
 theorem.  *}
 
-constdefs sq :: "'a::times => 'a"
-         "sq x == x*x"
+definition
+  sq :: "'a::times => 'a"
+  "sq x == x*x"
 
 text {* The following lemma essentially shows that every natural
 number is the sum of four squares, provided all prime numbers are.
@@ -26,7 +27,6 @@
 
 ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
 
--- {* once a slow step, but now (2001) just three seconds! *}
 lemma Lagrange_lemma:
  "!!x1::'a::comm_ring.
   (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/MonoidGroup.thy
--- a/src/HOL/ex/MonoidGroup.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/MonoidGroup.thy	Sat May 27 17:42:02 2006 +0200
@@ -14,17 +14,17 @@
 record 'a group_sig = "'a monoid_sig" +
   inv :: "'a => 'a"
 
-constdefs
+definition
   monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
-  "monoid M == \<forall>x y z.
+  "monoid M = (\<forall>x y z.
     times M (times M x y) z = times M x (times M y z) \<and>
-    times M (one M) x = x \<and> times M x (one M) = x"
+    times M (one M) x = x \<and> times M x (one M) = x)"
 
   group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
-  "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
+  "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
 
   reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
     (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
-  "reverse M == M (| times := \<lambda>x y. times M y x |)"
+  "reverse M = M (| times := \<lambda>x y. times M y x |)"
 
 end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/PER.thy	Sat May 27 17:42:02 2006 +0200
@@ -44,9 +44,9 @@
   \emph{any} other one.
 *}
 
-constdefs
-  domain :: "'a::partial_equiv set"
-  "domain == {x. x \<sim> x}"
+definition
+  "domain" :: "'a::partial_equiv set"
+  "domain = {x. x \<sim> x}"
 
 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
   by (unfold domain_def) blast
@@ -164,9 +164,9 @@
   representation of elements of a quotient type.
 *}
 
-constdefs
+definition
   eqv_class :: "('a::partial_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_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
 proof (cases A)
@@ -231,9 +231,9 @@
 
 subsection {* Picking representing elements *}
 
-constdefs
+definition
   pick :: "'a::partial_equiv quot => 'a"
-  "pick A == SOME a. A = \<lfloor>a\<rfloor>"
+  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
 
 theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a"
 proof (unfold pick_def)
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Primrec.thy	Sat May 27 17:42:02 2006 +0200
@@ -42,24 +42,24 @@
 
 text {* The set of primitive recursive functions of type @{typ "nat list => nat"}. *}
 
-constdefs
+definition
   SC :: "nat list => nat"
-  "SC l == Suc (zeroHd l)"
+  "SC l = Suc (zeroHd l)"
 
   CONSTANT :: "nat => nat list => nat"
-  "CONSTANT k l == k"
+  "CONSTANT k l = k"
 
   PROJ :: "nat => nat list => nat"
-  "PROJ i l == zeroHd (drop i l)"
+  "PROJ i l = zeroHd (drop i l)"
 
   COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat"
-  "COMP g fs l == g (map (\<lambda>f. f l) fs)"
+  "COMP g fs l = g (map (\<lambda>f. f l) fs)"
 
   PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat"
-  "PREC f g l ==
-    case l of
+  "PREC f g l =
+    (case l of
       [] => 0
-    | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x"
+    | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x)"
   -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *}
 
 consts PRIMREC :: "(nat list => nat) set"
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Records.thy	Sat May 27 17:42:02 2006 +0200
@@ -50,11 +50,11 @@
 
 subsubsection {* Record selection and record update *}
 
-constdefs
+definition
   getX :: "'a point_scheme => nat"
-  "getX r == xpos r"
+  "getX r = xpos r"
   setX :: "'a point_scheme => nat => 'a point_scheme"
-  "setX r n == r (| xpos := n |)"
+  "setX r n = r (| xpos := n |)"
 
 
 subsubsection {* Some lemmas about records *}
@@ -144,16 +144,16 @@
  \medskip Concrete records are type instances of record schemes.
 *}
 
-constdefs
+definition
   foo5 :: nat
-  "foo5 == getX (| xpos = 1, ypos = 0 |)"
+  "foo5 = getX (| xpos = 1, ypos = 0 |)"
 
 
 text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *}
 
-constdefs
+definition
   incX :: "'a point_scheme => 'a point_scheme"
-  "incX r == (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
+  "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
 
 lemma "incX r = setX r (Suc (getX r))"
   by (simp add: getX_def setX_def incX_def)
@@ -161,9 +161,9 @@
 
 text {* An alternative definition. *}
 
-constdefs
+definition
   incX' :: "'a point_scheme => 'a point_scheme"
-  "incX' r == r (| xpos := xpos r + 1 |)"
+  "incX' r = r (| xpos := xpos r + 1 |)"
 
 
 subsection {* Coloured points: record extension *}
@@ -193,9 +193,9 @@
  Functions on @{text point} schemes work for @{text cpoints} as well.
 *}
 
-constdefs
+definition
   foo10 :: nat
-  "foo10 == getX (| xpos = 2, ypos = 0, colour = Blue |)"
+  "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
 
 
 subsubsection {* Non-coercive structural subtyping *}
@@ -205,9 +205,9 @@
  Great!
 *}
 
-constdefs
+definition
   foo11 :: cpoint
-  "foo11 == setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
+  "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
 
 
 subsection {* Other features *}
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Sat May 27 17:42:02 2006 +0200
@@ -529,8 +529,9 @@
 "islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i \<noteq> 0 \<and> n0 \<le> n \<and> islintn (n+1,r))"
 "islintn (n0, t) = False"
 
-constdefs islint :: "intterm \<Rightarrow> bool"
-  "islint t \<equiv> islintn(0,t)"
+definition
+  islint :: "intterm \<Rightarrow> bool"
+  "islint t = islintn(0,t)"
 
 (* And the equivalence to the first definition *)
 lemma islinintterm_eq_islint: "islinintterm t = islint t"
@@ -728,8 +729,9 @@
   by (induct l t rule: lin_mul.induct) simp_all
 
 (* lin_neg neagtes a linear term *)
-constdefs lin_neg :: "intterm \<Rightarrow> intterm"
-"lin_neg i == lin_mul ((-1::int),i)"
+definition
+  lin_neg :: "intterm \<Rightarrow> intterm"
+  "lin_neg i = lin_mul ((-1::int),i)"
 
 (* lin_neg has the semantics of Neg *)
 lemma lin_neg_corr:
@@ -1622,11 +1624,13 @@
 by simp
 
 (* Definitions and lemmas about gcd and lcm *)
-constdefs lcm :: "nat \<times> nat \<Rightarrow> nat"
-  "lcm \<equiv> (\<lambda>(m,n). m*n div gcd(m,n))"
-
-constdefs ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
-  "ilcm \<equiv> \<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j)))"
+definition
+  lcm :: "nat \<times> nat \<Rightarrow> nat"
+  "lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
+
+definition
+  ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
+  "ilcm = (\<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j))))"
 
 (* ilcm_dvd12 are needed later *)
 lemma lcm_dvd1: 
@@ -1874,8 +1878,9 @@
 
 
 (* unitycoeff expects a quantifier free formula an transforms it to an equivalent formula where the bound variable occurs only with coeffitient 1  or -1 *)
-constdefs unitycoeff :: "QF \<Rightarrow> QF"
-  "unitycoeff p == 
+definition
+  unitycoeff :: "QF \<Rightarrow> QF"
+  "unitycoeff p =
   (let l = formlcm p;
        p' = adjustcoeff (l,p)
    in (if l=1 then p' else 
@@ -5085,8 +5090,9 @@
 
 
 (* An implementation of sets trough lists *)
-constdefs list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  "list_insert x xs \<equiv> (if x mem xs then xs else x#xs)"
+definition
+  list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  "list_insert x xs = (if x mem xs then xs else x#xs)"
 
 lemma list_insert_set: "set (list_insert x xs) = set (x#xs)"
 by(induct xs) (auto simp add: list_insert_def)
@@ -5362,8 +5368,8 @@
 (* An implementation of cooper's method for both plus/minus/infinity *)
 
 (* unify the formula *)
-constdefs unify:: "QF \<Rightarrow> (QF \<times> intterm list)"
-  "unify p \<equiv> 
+definition unify:: "QF \<Rightarrow> (QF \<times> intterm list)"
+  "unify p =
   (let q = unitycoeff p;
        B = list_set(bset q);
        A = list_set (aset q)
@@ -5477,8 +5483,9 @@
     using qB_def by simp
 qed
 (* An implementation of cooper's method *)
-constdefs cooper:: "QF \<Rightarrow> QF option"
-"cooper p \<equiv> lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
+definition
+  cooper:: "QF \<Rightarrow> QF option"
+  "cooper p = lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
 
 (* cooper eliminates quantifiers *)
 lemma cooper_qfree: "(\<And> q q'. \<lbrakk>isqfree q ; cooper q = Some q'\<rbrakk> \<Longrightarrow>  isqfree q')"
@@ -5530,8 +5537,9 @@
 qed  
 
 (* A decision procedure for Presburger Arithmetics *)
-constdefs pa:: "QF \<Rightarrow> QF option"
-"pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
+definition
+  pa:: "QF \<Rightarrow> QF option"
+  "pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
 
 lemma psimpl_qfree: "isqfree p \<Longrightarrow> isqfree (psimpl p)"
 apply(induct p rule: isqfree.induct)
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Sorting.thy	Sat May 27 17:42:02 2006 +0200
@@ -24,12 +24,12 @@
   "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
 
 
-constdefs
+definition
   total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
-   "total r == (\<forall>x y. r x y | r y x)"
+   "total r = (\<forall>x y. r x y | r y x)"
   
   transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
-   "transf f == (\<forall>x y z. f x y & f y z --> f x z)"
+   "transf f = (\<forall>x y z. f x y & f y z --> f x z)"
 
 
 
@@ -44,8 +44,8 @@
 done
 
 lemma sorted_append [simp]:
- "sorted le (xs@ys) = 
-  (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
-by (induct xs, auto)
+  "sorted le (xs@ys) = 
+    (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
+  by (induct xs) auto
 
 end
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Tarski.thy	Sat May 27 17:42:02 2006 +0200
@@ -20,79 +20,77 @@
   pset  :: "'a set"
   order :: "('a * 'a) set"
 
-constdefs
+definition
   monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
-  "monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
+  "monotone f A r = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r)"
 
   least :: "['a => bool, 'a potype] => 'a"
-  "least P po == @ x. x: pset po & P x &
-                       (\<forall>y \<in> pset po. P y --> (x,y): order po)"
+  "least P po = (SOME x. x: pset po & P x &
+                       (\<forall>y \<in> pset po. P y --> (x,y): order po))"
 
   greatest :: "['a => bool, 'a potype] => 'a"
-  "greatest P po == @ x. x: pset po & P x &
-                          (\<forall>y \<in> pset po. P y --> (y,x): order po)"
+  "greatest P po = (SOME x. x: pset po & P x &
+                          (\<forall>y \<in> pset po. P y --> (y,x): order po))"
 
   lub  :: "['a set, 'a potype] => 'a"
-  "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
+  "lub S po = least (%x. \<forall>y\<in>S. (y,x): order po) po"
 
   glb  :: "['a set, 'a potype] => 'a"
-  "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
+  "glb S po = greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
 
   isLub :: "['a set, 'a potype, 'a] => bool"
-  "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
-                   (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
+  "isLub S po = (%L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
+                   (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po)))"
 
   isGlb :: "['a set, 'a potype, 'a] => bool"
-  "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
-                 (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
+  "isGlb S po = (%G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
+                 (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po)))"
 
   "fix"    :: "[('a => 'a), 'a set] => 'a set"
-  "fix f A  == {x. x: A & f x = x}"
+  "fix f A  = {x. x: A & f x = x}"
 
   interval :: "[('a*'a) set,'a, 'a ] => 'a set"
-  "interval r a b == {x. (a,x): r & (x,b): r}"
+  "interval r a b = {x. (a,x): r & (x,b): r}"
 
 
-constdefs
+definition
   Bot :: "'a potype => 'a"
-  "Bot po == least (%x. True) po"
+  "Bot po = least (%x. True) po"
 
   Top :: "'a potype => 'a"
-  "Top po == greatest (%x. True) po"
+  "Top po = greatest (%x. True) po"
 
   PartialOrder :: "('a potype) set"
-  "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
+  "PartialOrder = {P. refl (pset P) (order P) & antisym (order P) &
                        trans (order P)}"
 
   CompleteLattice :: "('a potype) set"
-  "CompleteLattice == {cl. cl: PartialOrder &
+  "CompleteLattice = {cl. cl: PartialOrder &
                         (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) &
                         (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
 
   CLF :: "('a potype * ('a => 'a)) set"
-  "CLF == SIGMA cl: CompleteLattice.
-            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
+  "CLF = (SIGMA cl: CompleteLattice.
+            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
 
   induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
-  "induced A r == {(a,b). a : A & b: A & (a,b): r}"
+  "induced A r = {(a,b). a : A & b: A & (a,b): r}"
 
 
-constdefs
+definition
   sublattice :: "('a potype * 'a set)set"
-  "sublattice ==
-      SIGMA cl: CompleteLattice.
+  "sublattice =
+      (SIGMA cl: CompleteLattice.
           {S. S \<subseteq> pset cl &
-           (| pset = S, order = induced S (order cl) |): CompleteLattice }"
+           (| pset = S, order = induced S (order cl) |): CompleteLattice})"
 
-syntax
-  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
+abbreviation
+  sublat :: "['a set, 'a potype] => bool"  ("_ <<= _" [51,50]50)
+  "S <<= cl == S : sublattice `` {cl}"
 
-translations
-  "S <<= cl" == "S : sublattice `` {cl}"
-
-constdefs
+definition
   dual :: "'a potype => 'a potype"
-  "dual po == (| pset = pset po, order = converse (order po) |)"
+  "dual po = (| pset = pset po, order = converse (order po) |)"
 
 locale (open) PO =
   fixes cl :: "'a potype"
diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/ThreeDivides.thy	Sat May 27 17:42:02 2006 +0200
@@ -155,9 +155,9 @@
 text {* The function @{text "sumdig"} returns the sum of all digits in
 some number n. *}
 
-constdefs 
+definition
   sumdig :: "nat \<Rightarrow> nat"
-  "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
+  "sumdig n = (\<Sum>x < nlen n. n div 10^x mod 10)"
 
 text {* Some properties of these functions follow. *}