# HG changeset patch
# User haftmann
# Date 1283966603 -7200
# Node ID 3a15ee47c6106f48a2dd883ff7604ba9dfc0f2f9
# Parent  5a3bd2b7d0eec16525b3b86d257a92183d1525a9# Parent  9e58f0499f57f8cfd73ccaf46cbe533202fceb1d
merged

diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -31,10 +31,8 @@
 
 subsubsection{*"remove l x" erase the first element of "l" equal to "x"*}
 
-consts remove :: "'a list => 'a => 'a list"
-
-primrec
-"remove [] y = []"
+primrec remove :: "'a list => 'a => 'a list" where
+"remove [] y = []" |
 "remove (x#xs) y = (if x=y then xs else x # remove xs y)"
 
 lemma set_remove: "set (remove l x) <= set l"
@@ -348,13 +346,9 @@
 
 subsubsection{*knows without initState*}
 
-consts knows' :: "agent => event list => msg set"
-
-primrec
-knows'_Nil:
- "knows' A [] = {}"
-
-knows'_Cons0:
+primrec knows' :: "agent => event list => msg set" where
+  knows'_Nil: "knows' A [] = {}" |
+  knows'_Cons0:
  "knows' A (ev # evs) = (
    if A = Spy then (
      case ev of
@@ -426,10 +420,8 @@
 subsubsection{*maximum knowledge an agent can have
 includes messages sent to the agent*}
 
-consts knows_max' :: "agent => event list => msg set"
-
-primrec
-knows_max'_def_Nil: "knows_max' A [] = {}"
+primrec knows_max' :: "agent => event list => msg set" where
+knows_max'_def_Nil: "knows_max' A [] = {}" |
 knows_max'_def_Cons: "knows_max' A (ev # evs) = (
   if A=Spy then (
     case ev of
@@ -498,10 +490,8 @@
 
 subsubsection{*used without initState*}
 
-consts used' :: "event list => msg set"
-
-primrec
-"used' [] = {}"
+primrec used' :: "event list => msg set" where
+"used' [] = {}" |
 "used' (ev # evs) = (
   case ev of
     Says A B X => parts {X} Un used' evs
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Auth/Public.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -199,24 +199,32 @@
 knowledge of the Spy.  All other agents are automata, merely following the
 protocol.*}
 
-primrec
+term initState_Server
+
+overloading
+  initState \<equiv> initState
+begin
+
+primrec initState where
         (*Agents know their private key and all public keys*)
   initState_Server:
     "initState Server     =    
        {Key (priEK Server), Key (priSK Server)} \<union> 
        (Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)"
 
-  initState_Friend:
+| initState_Friend:
     "initState (Friend i) =    
        {Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union> 
        (Key ` range pubEK) \<union> (Key ` range pubSK)"
 
-  initState_Spy:
+| initState_Spy:
     "initState Spy        =    
        (Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union> 
        (Key ` shrK ` bad) \<union> 
        (Key ` range pubEK) \<union> (Key ` range pubSK)"
 
+end
+
 
 text{*These lemmas allow reasoning about @{term "used evs"} rather than
    @{term "knows Spy evs"}, which is useful when there are private Notes. 
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Auth/Shared.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -22,10 +22,17 @@
    done
 
 text{*Server knows all long-term keys; other agents know only their own*}
-primrec
+
+overloading
+  initState \<equiv> initState
+begin
+
+primrec initState where
   initState_Server:  "initState Server     = Key ` range shrK"
-  initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
-  initState_Spy:     "initState Spy        = Key`shrK`bad"
+| initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
+| initState_Spy:     "initState Spy        = Key`shrK`bad"
+
+end
 
 
 subsection{*Basic properties of shrK*}
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Auth/Smartcard/EventSC.thy
--- a/src/HOL/Auth/Smartcard/EventSC.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -19,7 +19,6 @@
     
 consts 
  bad     :: "agent set"  (*compromised agents*)
- knows   :: "agent => event list => msg set" (*agents' knowledge*)
  stolen    :: "card set" (* stolen smart cards *)
  cloned  :: "card set"   (* cloned smart cards*)
  secureM :: "bool"(*assumption of secure means between agents and their cards*)
@@ -50,7 +49,8 @@
 
 primrec (*This definition is extended over the new events, subject to the 
           assumption of secure means*)
-  knows_Nil:   "knows A [] = initState A"
+  knows   :: "agent => event list => msg set" (*agents' knowledge*) where
+  knows_Nil:   "knows A [] = initState A" |
   knows_Cons:  "knows A (ev # evs) =
          (case ev of
             Says A' B X => 
@@ -78,13 +78,11 @@
 
 
 
-consts
+primrec
   (*The set of items that might be visible to someone is easily extended 
     over the new events*)
-  used :: "event list => msg set"
-
-primrec
-  used_Nil:   "used []         = (UN B. parts (initState B))"
+  used :: "event list => msg set" where
+  used_Nil:   "used []         = (UN B. parts (initState B))" |
   used_Cons:  "used (ev # evs) =
                  (case ev of
                     Says A B X => parts {X} \<union> (used evs)
@@ -98,7 +96,6 @@
        Likewise, @{term C_Gets} will always have to follow @{term Inputs}
        and @{term A_Gets} will always have to follow @{term Outpts}*}
 
-
 lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs"
 apply (induct_tac evs)
 apply (auto split: event.split) 
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -51,16 +51,21 @@
 
 
 text{*initState must be defined with care*}
-primrec
+
+overloading
+  initState \<equiv> initState
+begin
+
+primrec initState where
 (*Server knows all long-term keys; adding cards' keys may be redundant but
   helps prove crdK_in_initState and crdK_in_used to distinguish cards' keys
   from fresh (session) keys*)
   initState_Server:  "initState Server = 
         (Key`(range shrK \<union> range crdK \<union> range pin \<union> range pairK)) \<union> 
-        (Nonce`(range Pairkey))"
+        (Nonce`(range Pairkey))" |
 
 (*Other agents know only their own*)
-  initState_Friend:  "initState (Friend i) = {Key (pin (Friend i))}"
+  initState_Friend:  "initState (Friend i) = {Key (pin (Friend i))}" |
 
 (*Spy knows bad agents' pins, cloned cards' keys, pairKs, and Pairkeys *)
   initState_Spy: "initState Spy  = 
@@ -70,6 +75,7 @@
                         (pairK`{(X,A). Card A \<in> cloned})))
            \<union> (Nonce`(Pairkey`{(A,B). Card A \<in> cloned & Card B \<in> cloned}))"
 
+end
 
 text{*Still relying on axioms*}
 axioms
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -67,27 +67,26 @@
   by (induct p rule: fmsize.induct) simp_all
 
   (* Semantics of formulae (fm) *)
-consts Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"
-primrec
+primrec Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool" where
   "Ifm bbs bs T = True"
-  "Ifm bbs bs F = False"
-  "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
-  "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
-  "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
-  "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
-  "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
-  "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
-  "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
-  "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
-  "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
-  "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
-  "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
-  "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
-  "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
-  "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
-  "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
-  "Ifm bbs bs (Closed n) = bbs!n"
-  "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
+| "Ifm bbs bs F = False"
+| "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
+| "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
+| "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
+| "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
+| "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
+| "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
+| "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
+| "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
+| "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
+| "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
+| "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
+| "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
+| "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
+| "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
+| "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
+| "Ifm bbs bs (Closed n) = bbs!n"
+| "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
 
 consts prep :: "fm \<Rightarrow> fm"
 recdef prep "measure fmsize"
@@ -132,50 +131,47 @@
   "qfree p = True"
 
   (* Boundedness and substitution *)
-consts 
-  numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
-  bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
-  subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
-primrec
+    
+primrec numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
   "numbound0 (C c) = True"
-  "numbound0 (Bound n) = (n>0)"
-  "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
-  "numbound0 (Neg a) = numbound0 a"
-  "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
-  "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
-  "numbound0 (Mul i a) = numbound0 a"
+| "numbound0 (Bound n) = (n>0)"
+| "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
+| "numbound0 (Neg a) = numbound0 a"
+| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
+| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
+| "numbound0 (Mul i a) = numbound0 a"
 
 lemma numbound0_I:
   assumes nb: "numbound0 a"
   shows "Inum (b#bs) a = Inum (b'#bs) a"
 using nb
-by (induct a rule: numbound0.induct) (auto simp add: gr0_conv_Suc)
+by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
 
-primrec
+primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
   "bound0 T = True"
-  "bound0 F = True"
-  "bound0 (Lt a) = numbound0 a"
-  "bound0 (Le a) = numbound0 a"
-  "bound0 (Gt a) = numbound0 a"
-  "bound0 (Ge a) = numbound0 a"
-  "bound0 (Eq a) = numbound0 a"
-  "bound0 (NEq a) = numbound0 a"
-  "bound0 (Dvd i a) = numbound0 a"
-  "bound0 (NDvd i a) = numbound0 a"
-  "bound0 (NOT p) = bound0 p"
-  "bound0 (And p q) = (bound0 p \<and> bound0 q)"
-  "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
-  "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
-  "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
-  "bound0 (E p) = False"
-  "bound0 (A p) = False"
-  "bound0 (Closed P) = True"
-  "bound0 (NClosed P) = True"
+| "bound0 F = True"
+| "bound0 (Lt a) = numbound0 a"
+| "bound0 (Le a) = numbound0 a"
+| "bound0 (Gt a) = numbound0 a"
+| "bound0 (Ge a) = numbound0 a"
+| "bound0 (Eq a) = numbound0 a"
+| "bound0 (NEq a) = numbound0 a"
+| "bound0 (Dvd i a) = numbound0 a"
+| "bound0 (NDvd i a) = numbound0 a"
+| "bound0 (NOT p) = bound0 p"
+| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
+| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
+| "bound0 (E p) = False"
+| "bound0 (A p) = False"
+| "bound0 (Closed P) = True"
+| "bound0 (NClosed P) = True"
 lemma bound0_I:
   assumes bp: "bound0 p"
   shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
 using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
-by (induct p rule: bound0.induct) (auto simp add: gr0_conv_Suc)
+by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
 
 fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
   "numsubst0 t (C c) = (C c)"
@@ -195,24 +191,24 @@
   "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
 by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
 
-primrec
+primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
   "subst0 t T = T"
-  "subst0 t F = F"
-  "subst0 t (Lt a) = Lt (numsubst0 t a)"
-  "subst0 t (Le a) = Le (numsubst0 t a)"
-  "subst0 t (Gt a) = Gt (numsubst0 t a)"
-  "subst0 t (Ge a) = Ge (numsubst0 t a)"
-  "subst0 t (Eq a) = Eq (numsubst0 t a)"
-  "subst0 t (NEq a) = NEq (numsubst0 t a)"
-  "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
-  "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
-  "subst0 t (NOT p) = NOT (subst0 t p)"
-  "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
-  "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
-  "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
-  "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
-  "subst0 t (Closed P) = (Closed P)"
-  "subst0 t (NClosed P) = (NClosed P)"
+| "subst0 t F = F"
+| "subst0 t (Lt a) = Lt (numsubst0 t a)"
+| "subst0 t (Le a) = Le (numsubst0 t a)"
+| "subst0 t (Gt a) = Gt (numsubst0 t a)"
+| "subst0 t (Ge a) = Ge (numsubst0 t a)"
+| "subst0 t (Eq a) = Eq (numsubst0 t a)"
+| "subst0 t (NEq a) = NEq (numsubst0 t a)"
+| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
+| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
+| "subst0 t (NOT p) = NOT (subst0 t p)"
+| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
+| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
+| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
+| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
+| "subst0 t (Closed P) = (Closed P)"
+| "subst0 t (NClosed P) = (NClosed P)"
 
 lemma subst0_I: assumes qfp: "qfree p"
   shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"
@@ -280,14 +276,14 @@
 
 lemma numsubst0_numbound0: assumes nb: "numbound0 t"
   shows "numbound0 (numsubst0 t a)"
-using nb apply (induct a rule: numbound0.induct)
+using nb apply (induct a)
 apply simp_all
-apply (case_tac n, simp_all)
+apply (case_tac nat, simp_all)
 done
 
 lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
   shows "bound0 (subst0 t p)"
-using qf numsubst0_numbound0[OF nb] by (induct p  rule: subst0.induct, auto)
+using qf numsubst0_numbound0[OF nb] by (induct p) auto
 
 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
 by (induct p, simp_all)
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -16,26 +16,24 @@
   | Neg tm | Sub tm tm | CNP nat poly tm
   (* A size for poly to make inductive proofs simpler*)
 
-consts tmsize :: "tm \<Rightarrow> nat"
-primrec 
+primrec tmsize :: "tm \<Rightarrow> nat" where
   "tmsize (CP c) = polysize c"
-  "tmsize (Bound n) = 1"
-  "tmsize (Neg a) = 1 + tmsize a"
-  "tmsize (Add a b) = 1 + tmsize a + tmsize b"
-  "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
-  "tmsize (Mul c a) = 1 + polysize c + tmsize a"
-  "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
+| "tmsize (Bound n) = 1"
+| "tmsize (Neg a) = 1 + tmsize a"
+| "tmsize (Add a b) = 1 + tmsize a + tmsize b"
+| "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
+| "tmsize (Mul c a) = 1 + polysize c + tmsize a"
+| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
 
   (* Semantics of terms tm *)
-consts Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
-primrec
+primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where
   "Itm vs bs (CP c) = (Ipoly vs c)"
-  "Itm vs bs (Bound n) = bs!n"
-  "Itm vs bs (Neg a) = -(Itm vs bs a)"
-  "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
-  "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
-  "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
-  "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"   
+| "Itm vs bs (Bound n) = bs!n"
+| "Itm vs bs (Neg a) = -(Itm vs bs a)"
+| "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
+| "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
+| "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
+| "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"   
 
 
 fun allpolys:: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool"  where
@@ -47,51 +45,48 @@
 | "allpolys P (Sub p q) = (allpolys P p \<and> allpolys P q)"
 | "allpolys P p = True"
 
-consts 
-  tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool"
-  tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *)
-  tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *)
-  incrtm0:: "tm \<Rightarrow> tm"
-  incrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm"
-  decrtm0:: "tm \<Rightarrow> tm" 
-  decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" 
-primrec
+primrec tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool" where
   "tmboundslt n (CP c) = True"
-  "tmboundslt n (Bound m) = (m < n)"
-  "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
-  "tmboundslt n (Neg a) = tmboundslt n a"
-  "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
-  "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 
-  "tmboundslt n (Mul i a) = tmboundslt n a"
-primrec
+| "tmboundslt n (Bound m) = (m < n)"
+| "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
+| "tmboundslt n (Neg a) = tmboundslt n a"
+| "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
+| "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 
+| "tmboundslt n (Mul i a) = tmboundslt n a"
+
+primrec tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *) where
   "tmbound0 (CP c) = True"
-  "tmbound0 (Bound n) = (n>0)"
-  "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
-  "tmbound0 (Neg a) = tmbound0 a"
-  "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
-  "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 
-  "tmbound0 (Mul i a) = tmbound0 a"
+| "tmbound0 (Bound n) = (n>0)"
+| "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
+| "tmbound0 (Neg a) = tmbound0 a"
+| "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
+| "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 
+| "tmbound0 (Mul i a) = tmbound0 a"
 lemma tmbound0_I:
   assumes nb: "tmbound0 a"
   shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
 using nb
-by (induct a rule: tmbound0.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto simp add: nth_pos2)
 
-primrec
+primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where
   "tmbound n (CP c) = True"
-  "tmbound n (Bound m) = (n \<noteq> m)"
-  "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
-  "tmbound n (Neg a) = tmbound n a"
-  "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
-  "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 
-  "tmbound n (Mul i a) = tmbound n a"
+| "tmbound n (Bound m) = (n \<noteq> m)"
+| "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
+| "tmbound n (Neg a) = tmbound n a"
+| "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
+| "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 
+| "tmbound n (Mul i a) = tmbound n a"
 lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t" by (induct t, auto)
 
 lemma tmbound_I: 
   assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound n t" and le: "n \<le> length bs"
   shows "Itm vs (bs[n:=x]) t = Itm vs bs t"
   using nb le bnd
-  by (induct t rule: tmbound.induct , auto)
+  by (induct t rule: tm.induct , auto)
+
+consts 
+  incrtm0:: "tm \<Rightarrow> tm"
+  decrtm0:: "tm \<Rightarrow> tm" 
 
 recdef decrtm0 "measure size"
   "decrtm0 (Bound n) = Bound (n - 1)"
@@ -101,6 +96,7 @@
   "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
   "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
   "decrtm0 a = a"
+
 recdef incrtm0 "measure size"
   "incrtm0 (Bound n) = Bound (n + 1)"
   "incrtm0 (Neg a) = Neg (incrtm0 a)"
@@ -109,25 +105,26 @@
   "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
   "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
   "incrtm0 a = a"
+
 lemma decrtm0: assumes nb: "tmbound0 t"
   shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
   using nb by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
+
 lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
   by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
 
-primrec
+primrec decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" where
   "decrtm m (CP c) = (CP c)"
-  "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
-  "decrtm m (Neg a) = Neg (decrtm m a)"
-  "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
-  "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
-  "decrtm m (Mul c a) = Mul c (decrtm m a)"
-  "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
+| "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
+| "decrtm m (Neg a) = Neg (decrtm m a)"
+| "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
+| "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
+| "decrtm m (Mul c a) = Mul c (decrtm m a)"
+| "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
 
-consts removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-primrec
+primrec removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "removen n [] = []"
-  "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
+| "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
 
 lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs"
   by (induct xs arbitrary: n, auto)
@@ -172,50 +169,47 @@
   and nle: "m \<le> length bs" 
   shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
   using bnd nb nle
-  by (induct t rule: decrtm.induct, auto simp add: removen_nth)
+  by (induct t rule: tm.induct, auto simp add: removen_nth)
 
-consts tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm"
-primrec
+primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where
   "tmsubst0 t (CP c) = CP c"
-  "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
-  "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
-  "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
-  "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
-  "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
-  "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
+| "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
+| "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
+| "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
+| "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
+| "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
+| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
 lemma tmsubst0:
   shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
-by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto simp add: nth_pos2)
 
 lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
-by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto simp add: nth_pos2)
 
-consts tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" 
-
-primrec
+primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
   "tmsubst n t (CP c) = CP c"
-  "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
-  "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 
+| "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
+| "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 
              else CNP m c (tmsubst n t a))"
-  "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
-  "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
-  "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
-  "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
+| "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
+| "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
+| "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
+| "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
 
 lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \<le> length bs"
   shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
 using nb nlt
-by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
+by (induct a rule: tm.induct,auto simp add: nth_pos2)
 
 lemma tmsubst_nb0: assumes tnb: "tmbound0 t"
 shows "tmbound0 (tmsubst 0 t a)"
 using tnb
-by (induct a rule: tmsubst.induct, auto)
+by (induct a rule: tm.induct, auto)
 
 lemma tmsubst_nb: assumes tnb: "tmbound m t"
 shows "tmbound m (tmsubst m t a)"
 using tnb
-by (induct a rule: tmsubst.induct, auto)
+by (induct a rule: tm.induct, auto)
 lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
   by (induct t, auto)
   (* Simplification *)
@@ -447,21 +441,20 @@
 by (induct p rule: fmsize.induct) simp_all
 
   (* Semantics of formulae (fm) *)
-consts Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
-primrec
+primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where
   "Ifm vs bs T = True"
-  "Ifm vs bs F = False"
-  "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
-  "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
-  "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
-  "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
-  "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
-  "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
-  "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
-  "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
-  "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
-  "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
-  "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
+| "Ifm vs bs F = False"
+| "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
+| "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
+| "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
+| "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
+| "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
+| "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
+| "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
+| "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
+| "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
+| "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
+| "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
 
 consts not:: "fm \<Rightarrow> fm"
 recdef not "measure size"
@@ -516,27 +509,24 @@
 
   (* Boundedness and substitution *)
 
-consts boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool"
-primrec
+primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool" where
   "boundslt n T = True"
-  "boundslt n F = True"
-  "boundslt n (Lt t) = (tmboundslt n t)"
-  "boundslt n (Le t) = (tmboundslt n t)"
-  "boundslt n (Eq t) = (tmboundslt n t)"
-  "boundslt n (NEq t) = (tmboundslt n t)"
-  "boundslt n (NOT p) = boundslt n p"
-  "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
-  "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
-  "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
-  "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
-  "boundslt n (E p) = boundslt (Suc n) p"
-  "boundslt n (A p) = boundslt (Suc n) p"
+| "boundslt n F = True"
+| "boundslt n (Lt t) = (tmboundslt n t)"
+| "boundslt n (Le t) = (tmboundslt n t)"
+| "boundslt n (Eq t) = (tmboundslt n t)"
+| "boundslt n (NEq t) = (tmboundslt n t)"
+| "boundslt n (NOT p) = boundslt n p"
+| "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
+| "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
+| "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
+| "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
+| "boundslt n (E p) = boundslt (Suc n) p"
+| "boundslt n (A p) = boundslt (Suc n) p"
 
 consts 
   bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
-  bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *)
   decr0 :: "fm \<Rightarrow> fm"
-  decr :: "nat \<Rightarrow> fm \<Rightarrow> fm"
 recdef bound0 "measure size"
   "bound0 T = True"
   "bound0 F = True"
@@ -556,26 +546,26 @@
 using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
 by (induct p rule: bound0.induct,auto simp add: nth_pos2)
 
-primrec
+primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) where
   "bound m T = True"
-  "bound m F = True"
-  "bound m (Lt t) = tmbound m t"
-  "bound m (Le t) = tmbound m t"
-  "bound m (Eq t) = tmbound m t"
-  "bound m (NEq t) = tmbound m t"
-  "bound m (NOT p) = bound m p"
-  "bound m (And p q) = (bound m p \<and> bound m q)"
-  "bound m (Or p q) = (bound m p \<and> bound m q)"
-  "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
-  "bound m (Iff p q) = (bound m p \<and> bound m q)"
-  "bound m (E p) = bound (Suc m) p"
-  "bound m (A p) = bound (Suc m) p"
+| "bound m F = True"
+| "bound m (Lt t) = tmbound m t"
+| "bound m (Le t) = tmbound m t"
+| "bound m (Eq t) = tmbound m t"
+| "bound m (NEq t) = tmbound m t"
+| "bound m (NOT p) = bound m p"
+| "bound m (And p q) = (bound m p \<and> bound m q)"
+| "bound m (Or p q) = (bound m p \<and> bound m q)"
+| "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
+| "bound m (Iff p q) = (bound m p \<and> bound m q)"
+| "bound m (E p) = bound (Suc m) p"
+| "bound m (A p) = bound (Suc m) p"
 
 lemma bound_I:
   assumes bnd: "boundslt (length bs) p" and nb: "bound n p" and le: "n \<le> length bs"
   shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p"
   using bnd nb le tmbound_I[where bs=bs and vs = vs]
-proof(induct p arbitrary: bs n rule: bound.induct)
+proof(induct p arbitrary: bs n rule: fm.induct)
   case (E p bs n) 
   {fix y
     from prems have bnd: "boundslt (length (y#bs)) p" 
@@ -607,26 +597,26 @@
   using nb 
   by (induct p rule: decr0.induct, simp_all add: decrtm0)
 
-primrec
+primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> fm" where
   "decr m T = T"
-  "decr m F = F"
-  "decr m (Lt t) = (Lt (decrtm m t))"
-  "decr m (Le t) = (Le (decrtm m t))"
-  "decr m (Eq t) = (Eq (decrtm m t))"
-  "decr m (NEq t) = (NEq (decrtm m t))"
-  "decr m (NOT p) = NOT (decr m p)" 
-  "decr m (And p q) = conj (decr m p) (decr m q)"
-  "decr m (Or p q) = disj (decr m p) (decr m q)"
-  "decr m (Imp p q) = imp (decr m p) (decr m q)"
-  "decr m (Iff p q) = iff (decr m p) (decr m q)"
-  "decr m (E p) = E (decr (Suc m) p)"
-  "decr m (A p) = A (decr (Suc m) p)"
+| "decr m F = F"
+| "decr m (Lt t) = (Lt (decrtm m t))"
+| "decr m (Le t) = (Le (decrtm m t))"
+| "decr m (Eq t) = (Eq (decrtm m t))"
+| "decr m (NEq t) = (NEq (decrtm m t))"
+| "decr m (NOT p) = NOT (decr m p)" 
+| "decr m (And p q) = conj (decr m p) (decr m q)"
+| "decr m (Or p q) = disj (decr m p) (decr m q)"
+| "decr m (Imp p q) = imp (decr m p) (decr m q)"
+| "decr m (Iff p q) = iff (decr m p) (decr m q)"
+| "decr m (E p) = E (decr (Suc m) p)"
+| "decr m (A p) = A (decr (Suc m) p)"
 
 lemma decr: assumes  bnd: "boundslt (length bs) p" and nb: "bound m p" 
   and nle: "m < length bs" 
   shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p"
   using bnd nb nle
-proof(induct p arbitrary: bs m rule: decr.induct)
+proof(induct p arbitrary: bs m rule: fm.induct)
   case (E p bs m) 
   {fix x
     from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
@@ -642,55 +632,51 @@
   } thus ?case by auto
 qed (auto simp add: decrtm removen_nth)
 
-consts
-  subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm"
-
-primrec
+primrec subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm" where
   "subst0 t T = T"
-  "subst0 t F = F"
-  "subst0 t (Lt a) = Lt (tmsubst0 t a)"
-  "subst0 t (Le a) = Le (tmsubst0 t a)"
-  "subst0 t (Eq a) = Eq (tmsubst0 t a)"
-  "subst0 t (NEq a) = NEq (tmsubst0 t a)"
-  "subst0 t (NOT p) = NOT (subst0 t p)"
-  "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
-  "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
-  "subst0 t (Imp p q) = Imp (subst0 t p)  (subst0 t q)"
-  "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
-  "subst0 t (E p) = E p"
-  "subst0 t (A p) = A p"
+| "subst0 t F = F"
+| "subst0 t (Lt a) = Lt (tmsubst0 t a)"
+| "subst0 t (Le a) = Le (tmsubst0 t a)"
+| "subst0 t (Eq a) = Eq (tmsubst0 t a)"
+| "subst0 t (NEq a) = NEq (tmsubst0 t a)"
+| "subst0 t (NOT p) = NOT (subst0 t p)"
+| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
+| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
+| "subst0 t (Imp p q) = Imp (subst0 t p)  (subst0 t q)"
+| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
+| "subst0 t (E p) = E p"
+| "subst0 t (A p) = A p"
 
 lemma subst0: assumes qf: "qfree p"
   shows "Ifm vs (x#bs) (subst0 t p) = Ifm vs ((Itm vs (x#bs) t)#bs) p"
 using qf tmsubst0[where x="x" and bs="bs" and t="t"]
-by (induct p rule: subst0.induct, auto)
+by (induct p rule: fm.induct, auto)
 
 lemma subst0_nb:
   assumes bp: "tmbound0 t" and qf: "qfree p"
   shows "bound0 (subst0 t p)"
 using qf tmsubst0_nb[OF bp] bp
-by (induct p rule: subst0.induct, auto)
+by (induct p rule: fm.induct, auto)
 
-consts   subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" 
-primrec
+primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" where
   "subst n t T = T"
-  "subst n t F = F"
-  "subst n t (Lt a) = Lt (tmsubst n t a)"
-  "subst n t (Le a) = Le (tmsubst n t a)"
-  "subst n t (Eq a) = Eq (tmsubst n t a)"
-  "subst n t (NEq a) = NEq (tmsubst n t a)"
-  "subst n t (NOT p) = NOT (subst n t p)"
-  "subst n t (And p q) = And (subst n t p) (subst n t q)"
-  "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
-  "subst n t (Imp p q) = Imp (subst n t p)  (subst n t q)"
-  "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
-  "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
-  "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
+| "subst n t F = F"
+| "subst n t (Lt a) = Lt (tmsubst n t a)"
+| "subst n t (Le a) = Le (tmsubst n t a)"
+| "subst n t (Eq a) = Eq (tmsubst n t a)"
+| "subst n t (NEq a) = NEq (tmsubst n t a)"
+| "subst n t (NOT p) = NOT (subst n t p)"
+| "subst n t (And p q) = And (subst n t p) (subst n t q)"
+| "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
+| "subst n t (Imp p q) = Imp (subst n t p)  (subst n t q)"
+| "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
+| "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
+| "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
 
 lemma subst: assumes nb: "boundslt (length bs) p" and nlm: "n \<le> length bs"
   shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p"
   using nb nlm
-proof (induct p arbitrary: bs n t rule: subst0.induct)
+proof (induct p arbitrary: bs n t rule: fm.induct)
   case (E p bs n) 
   {fix x 
     from prems have bn: "boundslt (length (x#bs)) p" by simp 
@@ -713,7 +699,7 @@
 lemma subst_nb: assumes tnb: "tmbound m t"
 shows "bound m (subst m t p)"
 using tnb tmsubst_nb incrtm0_tmbound
-by (induct p arbitrary: m t rule: subst.induct, auto)
+by (induct p arbitrary: m t rule: fm.induct, auto)
 
 lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
 by (induct p rule: not.induct, auto)
@@ -2475,10 +2461,9 @@
 
 text {* Rest of the implementation *}
 
-consts alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"
-primrec
+primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
   "alluopairs [] = []"
-  "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
+| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
 
 lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
 by (induct xs, auto)
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -10,60 +10,52 @@
 
 text{* Application of polynomial as a real function. *}
 
-consts poly :: "'a list => 'a  => ('a::{comm_ring})"
-primrec
+primrec poly :: "'a list => 'a  => ('a::{comm_ring})" where
   poly_Nil:  "poly [] x = 0"
-  poly_Cons: "poly (h#t) x = h + x * poly t x"
+| poly_Cons: "poly (h#t) x = h + x * poly t x"
 
 
 subsection{*Arithmetic Operations on Polynomials*}
 
 text{*addition*}
-consts padd :: "['a list, 'a list] => ('a::comm_ring_1) list"  (infixl "+++" 65)
-primrec
+primrec padd :: "['a list, 'a list] => ('a::comm_ring_1) list"  (infixl "+++" 65) where
   padd_Nil:  "[] +++ l2 = l2"
-  padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
+| padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
                             else (h + hd l2)#(t +++ tl l2))"
 
 text{*Multiplication by a constant*}
-consts cmult :: "['a :: comm_ring_1, 'a list] => 'a list"  (infixl "%*" 70)
-primrec
-   cmult_Nil:  "c %* [] = []"
-   cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
+primrec cmult :: "['a :: comm_ring_1, 'a list] => 'a list"  (infixl "%*" 70) where
+  cmult_Nil:  "c %* [] = []"
+| cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
 
 text{*Multiplication by a polynomial*}
-consts pmult :: "['a list, 'a list] => ('a::comm_ring_1) list"  (infixl "***" 70)
-primrec
-   pmult_Nil:  "[] *** l2 = []"
-   pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
+primrec pmult :: "['a list, 'a list] => ('a::comm_ring_1) list"  (infixl "***" 70) where
+  pmult_Nil:  "[] *** l2 = []"
+| pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
                               else (h %* l2) +++ ((0) # (t *** l2)))"
 
 text{*Repeated multiplication by a polynomial*}
-consts mulexp :: "[nat, 'a list, 'a  list] => ('a ::comm_ring_1) list"
-primrec
-   mulexp_zero:  "mulexp 0 p q = q"
-   mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
+primrec mulexp :: "[nat, 'a list, 'a  list] => ('a ::comm_ring_1) list" where
+  mulexp_zero:  "mulexp 0 p q = q"
+| mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
 
 text{*Exponential*}
-consts pexp :: "['a list, nat] => ('a::comm_ring_1) list"  (infixl "%^" 80)
-primrec
-   pexp_0:   "p %^ 0 = [1]"
-   pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
+primrec pexp :: "['a list, nat] => ('a::comm_ring_1) list"  (infixl "%^" 80) where
+  pexp_0:   "p %^ 0 = [1]"
+| pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
 
 text{*Quotient related value of dividing a polynomial by x + a*}
 (* Useful for divisor properties in inductive proofs *)
-consts "pquot" :: "['a list, 'a::field] => 'a list"
-primrec
-   pquot_Nil:  "pquot [] a= []"
-   pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
+primrec pquot :: "['a list, 'a::field] => 'a list" where
+  pquot_Nil:  "pquot [] a= []"
+| pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
                    else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
 
 
 text{*normalization of polynomials (remove extra 0 coeff)*}
-consts pnormalize :: "('a::comm_ring_1) list => 'a list"
-primrec
-   pnormalize_Nil:  "pnormalize [] = []"
-   pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
+primrec pnormalize :: "('a::comm_ring_1) list => 'a list" where
+  pnormalize_Nil:  "pnormalize [] = []"
+| pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
                                      then (if (h = 0) then [] else [h])
                                      else (h#(pnormalize p)))"
 
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -19,38 +19,35 @@
 abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
 
 subsection{* Boundedness, substitution and all that *}
-consts polysize:: "poly \<Rightarrow> nat"
-primrec
+primrec polysize:: "poly \<Rightarrow> nat" where
   "polysize (C c) = 1"
-  "polysize (Bound n) = 1"
-  "polysize (Neg p) = 1 + polysize p"
-  "polysize (Add p q) = 1 + polysize p + polysize q"
-  "polysize (Sub p q) = 1 + polysize p + polysize q"
-  "polysize (Mul p q) = 1 + polysize p + polysize q"
-  "polysize (Pw p n) = 1 + polysize p"
-  "polysize (CN c n p) = 4 + polysize c + polysize p"
+| "polysize (Bound n) = 1"
+| "polysize (Neg p) = 1 + polysize p"
+| "polysize (Add p q) = 1 + polysize p + polysize q"
+| "polysize (Sub p q) = 1 + polysize p + polysize q"
+| "polysize (Mul p q) = 1 + polysize p + polysize q"
+| "polysize (Pw p n) = 1 + polysize p"
+| "polysize (CN c n p) = 4 + polysize c + polysize p"
 
-consts 
-  polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *)
-  polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *)
-primrec
+primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where
   "polybound0 (C c) = True"
-  "polybound0 (Bound n) = (n>0)"
-  "polybound0 (Neg a) = polybound0 a"
-  "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
-  "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" 
-  "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
-  "polybound0 (Pw p n) = (polybound0 p)"
-  "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
-primrec
+| "polybound0 (Bound n) = (n>0)"
+| "polybound0 (Neg a) = polybound0 a"
+| "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
+| "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" 
+| "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
+| "polybound0 (Pw p n) = (polybound0 p)"
+| "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
+
+primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where
   "polysubst0 t (C c) = (C c)"
-  "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
-  "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
-  "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
-  "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" 
-  "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
-  "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
-  "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
+| "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
+| "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
+| "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
+| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" 
+| "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
+| "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
+| "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
                              else CN (polysubst0 t c) n (polysubst0 t p))"
 
 consts 
@@ -195,11 +192,10 @@
 
 definition shift1 :: "poly \<Rightarrow> poly" where
   "shift1 p \<equiv> CN 0\<^sub>p 0 p"
-consts funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
 
-primrec
-  "funpow 0 f x = x"
-  "funpow (Suc n) f x = funpow n f (f x)"
+abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
+  "funpow \<equiv> compow"
+
 function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)"
   where
   "polydivide_aux (a,n,p,k,s) = 
@@ -211,7 +207,6 @@
   else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
   by pat_completeness auto
 
-
 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
   "polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)"
 
@@ -230,16 +225,16 @@
 
 subsection{* Semantics of the polynomial representation *}
 
-consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}"
-primrec
+primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
   "Ipoly bs (C c) = INum c"
-  "Ipoly bs (Bound n) = bs!n"
-  "Ipoly bs (Neg a) = - Ipoly bs a"
-  "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
-  "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
-  "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
-  "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
-  "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
+| "Ipoly bs (Bound n) = bs!n"
+| "Ipoly bs (Neg a) = - Ipoly bs a"
+| "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
+| "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
+| "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
+| "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
+| "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
+
 abbreviation
   Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
   where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
@@ -729,7 +724,7 @@
   by (simp add: shift1_def)
 lemma funpow_shift1_isnpoly: 
   "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"
-  by (induct n arbitrary: p, auto simp add: shift1_isnpoly)
+  by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
 
 lemma funpow_isnpolyh: 
   assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"
@@ -767,7 +762,7 @@
 
 subsection{* Miscilanious lemmas about indexes, decrementation, substitution  etc ... *}
 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
-proof(induct p arbitrary: n rule: polybound0.induct, auto)
+proof(induct p arbitrary: n rule: poly.induct, auto)
   case (goal1 c n p n')
   hence "n = Suc (n - 1)" by simp
   hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
@@ -793,7 +788,7 @@
   assumes nb: "polybound0 a"
   shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
 using nb
-by (induct a rule: polybound0.induct) auto 
+by (induct a rule: poly.induct) auto 
 lemma polysubst0_I:
   shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
   by (induct t) simp_all
@@ -809,12 +804,12 @@
 
 lemma polysubst0_polybound0: assumes nb: "polybound0 t"
   shows "polybound0 (polysubst0 t a)"
-using nb by (induct a rule: polysubst0.induct, auto)
+using nb by (induct a rule: poly.induct, auto)
 
 lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
   by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
 
-fun maxindex :: "poly \<Rightarrow> nat" where
+primrec maxindex :: "poly \<Rightarrow> nat" where
   "maxindex (Bound n) = n + 1"
 | "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
 | "maxindex (Add p q) = max (maxindex p) (maxindex q)"
@@ -1183,7 +1178,7 @@
   case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
     and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
-  thus ?case by simp
+  thus ?case by (simp add: funpow_swap1)
 qed auto  
 
 lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
@@ -1641,8 +1636,8 @@
 
 lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
   unfolding pnormal_def
- apply (induct p rule: pnormalize.induct, simp_all)
- apply (case_tac "p=[]", simp_all)
+ apply (induct p)
+ apply (simp_all, case_tac "p=[]", simp_all)
  done
 
 lemma degree_degree: assumes inc: "isnonconstant p"
@@ -1668,16 +1663,15 @@
 qed
 
 section{* Swaps ; Division by a certain variable *}
-consts swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
-primrec
+primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
   "swap n m (C x) = C x"
-  "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
-  "swap n m (Neg t) = Neg (swap n m t)"
-  "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
-  "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
-  "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
-  "swap n m (Pw t k) = Pw (swap n m t) k"
-  "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k)
+| "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
+| "swap n m (Neg t) = Neg (swap n m t)"
+| "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
+| "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
+| "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
+| "swap n m (Pw t k) = Pw (swap n m t) k"
+| "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k)
   (swap n m p)"
 
 lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Hoare_Parallel/OG_Com.thy
--- a/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -32,24 +32,21 @@
 text {* The function @{text pre} extracts the precondition of an
 annotated command: *}
 
-consts
-  pre ::"'a ann_com \<Rightarrow> 'a assn" 
-primrec 
+primrec pre ::"'a ann_com \<Rightarrow> 'a assn"  where
   "pre (AnnBasic r f) = r"
-  "pre (AnnSeq c1 c2) = pre c1"
-  "pre (AnnCond1 r b c1 c2) = r"
-  "pre (AnnCond2 r b c) = r"
-  "pre (AnnWhile r b i c) = r"
-  "pre (AnnAwait r b c) = r"
+| "pre (AnnSeq c1 c2) = pre c1"
+| "pre (AnnCond1 r b c1 c2) = r"
+| "pre (AnnCond2 r b c) = r"
+| "pre (AnnWhile r b i c) = r"
+| "pre (AnnAwait r b c) = r"
 
 text {* Well-formedness predicate for atomic programs: *}
 
-consts atom_com :: "'a com \<Rightarrow> bool"
-primrec  
+primrec atom_com :: "'a com \<Rightarrow> bool" where
   "atom_com (Parallel Ts) = False"
-  "atom_com (Basic f) = True"
-  "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
-  "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
-  "atom_com (While b i c) = atom_com c"
+| "atom_com (Basic f) = True"
+| "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
+| "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
+| "atom_com (While b i c) = atom_com c"
   
 end
\ No newline at end of file
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Hoare_Parallel/OG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -3,29 +3,27 @@
 
 theory OG_Hoare imports OG_Tran begin
 
-consts assertions :: "'a ann_com \<Rightarrow> ('a assn) set"
-primrec
+primrec assertions :: "'a ann_com \<Rightarrow> ('a assn) set" where
   "assertions (AnnBasic r f) = {r}"
-  "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2"
-  "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
-  "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
-  "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
-  "assertions (AnnAwait r b c) = {r}" 
+| "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2"
+| "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2"
+| "assertions (AnnCond2 r b c) = {r} \<union> assertions c"
+| "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c"
+| "assertions (AnnAwait r b c) = {r}" 
 
-consts atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set"       
-primrec
+primrec atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set" where
   "atomics (AnnBasic r f) = {(r, Basic f)}"
-  "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
-  "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
-  "atomics (AnnCond2 r b c) = atomics c"
-  "atomics (AnnWhile r b i c) = atomics c" 
-  "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
+| "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2"
+| "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2"
+| "atomics (AnnCond2 r b c) = atomics c"
+| "atomics (AnnWhile r b i c) = atomics c" 
+| "atomics (AnnAwait r b c) = {(r \<inter> b, c)}"
 
-consts com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op"
-primrec "com (c, q) = c"
+primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
+  "com (c, q) = c"
 
-consts post :: "'a ann_triple_op \<Rightarrow> 'a assn"
-primrec "post (c, q) = q"
+primrec post :: "'a ann_triple_op \<Rightarrow> 'a assn" where
+  "post (c, q) = q"
 
 definition interfree_aux :: "('a ann_com_op \<times> 'a assn \<times> 'a ann_com_op) \<Rightarrow> bool" where
   "interfree_aux \<equiv> \<lambda>(co, q, co'). co'= None \<or>  
@@ -466,4 +464,4 @@
 apply(auto simp add: SEM_def sem_def)
 done
 
-end
\ No newline at end of file
+end
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/IMP/Compiler0.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/IMP/Compiler.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, TUM
     Copyright   1996 TUM
 
@@ -49,14 +48,13 @@
 
 subsection "The compiler"
 
-consts compile :: "com \<Rightarrow> instr list"
-primrec
-"compile \<SKIP> = []"
-"compile (x:==a) = [ASIN x a]"
-"compile (c1;c2) = compile c1 @ compile c2"
+primrec compile :: "com \<Rightarrow> instr list" where
+"compile \<SKIP> = []" |
+"compile (x:==a) = [ASIN x a]" |
+"compile (c1;c2) = compile c1 @ compile c2" |
 "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
  [JMPF b (length(compile c1) + 2)] @ compile c1 @
- [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
+ [JMPF (%x. False) (length(compile c2)+1)] @ compile c2" |
 "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
  [JMPB (length(compile c)+1)]"
 
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -33,17 +33,13 @@
 (*lemma INL_neq_INR: "ALL v1 v2. Sum_Type.Inr v2 ~= Sum_Type.Inl v1"
   by simp*)
 
-consts
-  ISL :: "'a + 'b => bool"
-  ISR :: "'a + 'b => bool"
-
-primrec ISL_def:
+primrec ISL :: "'a + 'b => bool" where
   "ISL (Inl x) = True"
-  "ISL (Inr x) = False"
+| "ISL (Inr x) = False"
 
-primrec ISR_def:
+primrec ISR :: "'a + 'b => bool" where
   "ISR (Inl x) = False"
-  "ISR (Inr x) = True"
+| "ISR (Inr x) = True"
 
 lemma ISL: "(ALL x. ISL (Inl x)) & (ALL y. ~ISL (Inr y))"
   by simp
@@ -51,14 +47,10 @@
 lemma ISR: "(ALL x. ISR (Inr x)) & (ALL y. ~ISR (Inl y))"
   by simp
 
-consts
-  OUTL :: "'a + 'b => 'a"
-  OUTR :: "'a + 'b => 'b"
-
-primrec OUTL_def:
+primrec OUTL :: "'a + 'b => 'a" where
   "OUTL (Inl x) = x"
 
-primrec OUTR_def:
+primrec OUTR :: "'a + 'b => 'b" where
   "OUTR (Inr x) = x"
 
 lemma OUTL: "OUTL (Inl x) = x"
@@ -79,17 +71,13 @@
 lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
   by simp
 
-consts
-  IS_SOME :: "'a option => bool"
-  IS_NONE :: "'a option => bool"
-
-primrec IS_SOME_def:
+primrec IS_SOME :: "'a option => bool" where
   "IS_SOME (Some x) = True"
-  "IS_SOME None = False"
+| "IS_SOME None = False"
 
-primrec IS_NONE_def:
+primrec IS_NONE :: "'a option => bool" where
   "IS_NONE (Some x) = False"
-  "IS_NONE None = True"
+| "IS_NONE None = True"
 
 lemma IS_NONE_DEF: "(!x. IS_NONE (Some x) = False) & (IS_NONE None = True)"
   by simp
@@ -97,15 +85,12 @@
 lemma IS_SOME_DEF: "(!x. IS_SOME (Some x) = True) & (IS_SOME None = False)"
   by simp
 
-consts
-  OPTION_JOIN :: "'a option option => 'a option"
-
-primrec OPTION_JOIN_def:
+primrec OPTION_JOIN :: "'a option option => 'a option" where
   "OPTION_JOIN None = None"
-  "OPTION_JOIN (Some x) = x"
+| "OPTION_JOIN (Some x) = x"
 
 lemma OPTION_JOIN_DEF: "(OPTION_JOIN None = None) & (ALL x. OPTION_JOIN (Some x) = x)"
-  by simp;
+  by simp
 
 lemma PAIR: "(fst x,snd x) = x"
   by simp
@@ -261,14 +246,11 @@
 lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
   by simp
 
-consts
-  list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat"
+primrec list_size :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
+  "list_size f [] = 0"
+| "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
 
-primrec
-  "list_size f [] = 0"
-  "list_size f (a0#a1) = 1 + (f a0 + list_size f a1)"
-
-lemma list_size_def: "(!f. list_size f [] = 0) &
+lemma list_size_def': "(!f. list_size f [] = 0) &
          (!f a0 a1. list_size f (a0#a1) = 1 + (f a0 + list_size f a1))"
   by simp
 
@@ -377,12 +359,9 @@
 lemma list_exists_DEF: "(!P. list_ex P [] = False) & (!P h t. list_ex P (h#t) = (P h | list_ex P t))"
   by simp
 
-consts
-  map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list"
-
-primrec
+primrec map2 :: "[['a,'b]\<Rightarrow>'c,'a list,'b list] \<Rightarrow> 'c list" where
   map2_Nil: "map2 f [] l2 = []"
-  map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
+| map2_Cons: "map2 f (x#xs) l2 = f x (hd l2) # map2 f xs (tl l2)"
 
 lemma MAP2: "(!f. map2 f [] [] = []) & (!f h1 t1 h2 t2. map2 f (h1#t1) (h2#t2) = f h1 h2#map2 f t1 t2)"
   by simp
@@ -419,12 +398,9 @@
 lemma [hol4rew]: "ZIP (a,b) = zip a b"
   by (simp add: ZIP_def)
 
-consts
-  unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list"
-
-primrec
+primrec unzip :: "('a * 'b) list \<Rightarrow> 'a list * 'b list" where
   unzip_Nil: "unzip [] = ([],[])"
-  unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
+| unzip_Cons: "unzip (xy#xys) = (let zs = unzip xys in (fst xy # fst zs,snd xy # snd zs))"
 
 lemma UNZIP: "(unzip [] = ([],[])) &
          (!x l. unzip (x#l) = (fst x#fst (unzip l),snd x#snd (unzip l)))"
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Induct/ABexp.thy
--- a/src/HOL/Induct/ABexp.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Induct/ABexp.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -20,38 +20,32 @@
 
 text {* \medskip Evaluation of arithmetic and boolean expressions *}
 
-consts
-  evala :: "('a => nat) => 'a aexp => nat"
-  evalb :: "('a => nat) => 'a bexp => bool"
-
-primrec
+primrec evala :: "('a => nat) => 'a aexp => nat"
+  and evalb :: "('a => nat) => 'a bexp => bool" where
   "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
-  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
-  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
-  "evala env (Var v) = env v"
-  "evala env (Num n) = n"
+| "evala env (Sum a1 a2) = evala env a1 + evala env a2"
+| "evala env (Diff a1 a2) = evala env a1 - evala env a2"
+| "evala env (Var v) = env v"
+| "evala env (Num n) = n"
 
-  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
-  "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
-  "evalb env (Neg b) = (\<not> evalb env b)"
+| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
+| "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
+| "evalb env (Neg b) = (\<not> evalb env b)"
 
 
 text {* \medskip Substitution on arithmetic and boolean expressions *}
 
-consts
-  substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
-  substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
-
-primrec
+primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
+  and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp" where
   "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
-  "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
-  "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
-  "substa f (Var v) = f v"
-  "substa f (Num n) = Num n"
+| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
+| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
+| "substa f (Var v) = f v"
+| "substa f (Num n) = Num n"
 
-  "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
-  "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
-  "substb f (Neg b) = Neg (substb f b)"
+| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
+| "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
+| "substb f (Neg b) = Neg (substb f b)"
 
 lemma subst1_aexp:
   "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Induct/Ordinals.thy
--- a/src/HOL/Induct/Ordinals.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Induct/Ordinals.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -17,18 +17,13 @@
   | Succ ordinal
   | Limit "nat => ordinal"
 
-consts
-  pred :: "ordinal => nat => ordinal option"
-primrec
+primrec pred :: "ordinal => nat => ordinal option" where
   "pred Zero n = None"
-  "pred (Succ a) n = Some a"
-  "pred (Limit f) n = Some (f n)"
+| "pred (Succ a) n = Some a"
+| "pred (Limit f) n = Some (f n)"
 
-consts
-  iter :: "('a => 'a) => nat => ('a => 'a)"
-primrec
-  "iter f 0 = id"
-  "iter f (Suc n) = f \<circ> (iter f n)"
+abbreviation (input) iter :: "('a => 'a) => nat => ('a => 'a)" where
+  "iter f n \<equiv> f ^^ n"
 
 definition
   OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)" where
@@ -38,30 +33,24 @@
   OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>") where
   "\<Squnion>f = OpLim (iter f)"
 
-consts
-  cantor :: "ordinal => ordinal => ordinal"
-primrec
+primrec cantor :: "ordinal => ordinal => ordinal" where
   "cantor a Zero = Succ a"
-  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
-  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
+| "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
+| "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
 
-consts
-  Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>")
-primrec
+primrec Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>") where
   "\<nabla>f Zero = f Zero"
-  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
-  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
+| "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
+| "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
 
 definition
   deriv :: "(ordinal => ordinal) => (ordinal => ordinal)" where
   "deriv f = \<nabla>(\<Squnion>f)"
 
-consts
-  veblen :: "ordinal => ordinal => ordinal"
-primrec
+primrec veblen :: "ordinal => ordinal => ordinal" where
   "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
-  "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
-  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
+| "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
+| "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
 
 definition "veb a = veblen a Zero"
 definition "\<epsilon>\<^isub>0 = veb Zero"
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Induct/PropLog.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -41,25 +41,20 @@
 
 subsubsection {* Semantics of propositional logic. *}
 
-consts
-  eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100)
-
-primrec     "tt[[false]] = False"
-            "tt[[#v]]    = (v \<in> tt)"
-  eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
+primrec eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100) where
+            "tt[[false]] = False"
+|            "tt[[#v]]    = (v \<in> tt)"
+| eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
 
 text {*
   A finite set of hypotheses from @{text t} and the @{text Var}s in
   @{text p}.
 *}
 
-consts
-  hyps  :: "['a pl, 'a set] => 'a pl set"
-
-primrec
+primrec hyps  :: "['a pl, 'a set] => 'a pl set" where
   "hyps false  tt = {}"
-  "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
-  "hyps (p->q) tt = hyps p tt Un hyps q tt"
+| "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
+| "hyps (p->q) tt = hyps p tt Un hyps q tt"
 
 subsubsection {* Logical consequence *}
 
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Induct/QuoDataType.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -58,14 +58,11 @@
 
 text{*A function to return the set of nonces present in a message.  It will
 be lifted to the initial algrebra, to serve as an example of that process.*}
-consts
-  freenonces :: "freemsg \<Rightarrow> nat set"
-
-primrec
-   "freenonces (NONCE N) = {N}"
-   "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
-   "freenonces (CRYPT K X) = freenonces X"
-   "freenonces (DECRYPT K X) = freenonces X"
+primrec freenonces :: "freemsg \<Rightarrow> nat set" where
+  "freenonces (NONCE N) = {N}"
+| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
+| "freenonces (CRYPT K X) = freenonces X"
+| "freenonces (DECRYPT K X) = freenonces X"
 
 text{*This theorem lets us prove that the nonces function respects the
 equivalence relation.  It also helps us prove that Nonce
@@ -78,12 +75,11 @@
 
 text{*A function to return the left part of the top pair in a message.  It will
 be lifted to the initial algrebra, to serve as an example of that process.*}
-consts freeleft :: "freemsg \<Rightarrow> freemsg"
-primrec
-   "freeleft (NONCE N) = NONCE N"
-   "freeleft (MPAIR X Y) = X"
-   "freeleft (CRYPT K X) = freeleft X"
-   "freeleft (DECRYPT K X) = freeleft X"
+primrec freeleft :: "freemsg \<Rightarrow> freemsg" where
+  "freeleft (NONCE N) = NONCE N"
+| "freeleft (MPAIR X Y) = X"
+| "freeleft (CRYPT K X) = freeleft X"
+| "freeleft (DECRYPT K X) = freeleft X"
 
 text{*This theorem lets us prove that the left function respects the
 equivalence relation.  It also helps us prove that MPair
@@ -96,12 +92,11 @@
 subsubsection{*The Right Projection*}
 
 text{*A function to return the right part of the top pair in a message.*}
-consts freeright :: "freemsg \<Rightarrow> freemsg"
-primrec
-   "freeright (NONCE N) = NONCE N"
-   "freeright (MPAIR X Y) = Y"
-   "freeright (CRYPT K X) = freeright X"
-   "freeright (DECRYPT K X) = freeright X"
+primrec freeright :: "freemsg \<Rightarrow> freemsg" where
+  "freeright (NONCE N) = NONCE N"
+| "freeright (MPAIR X Y) = Y"
+| "freeright (CRYPT K X) = freeright X"
+| "freeright (DECRYPT K X) = freeright X"
 
 text{*This theorem lets us prove that the right function respects the
 equivalence relation.  It also helps us prove that MPair
@@ -114,12 +109,11 @@
 subsubsection{*The Discriminator for Constructors*}
 
 text{*A function to distinguish nonces, mpairs and encryptions*}
-consts freediscrim :: "freemsg \<Rightarrow> int"
-primrec
-   "freediscrim (NONCE N) = 0"
-   "freediscrim (MPAIR X Y) = 1"
-   "freediscrim (CRYPT K X) = freediscrim X + 2"
-   "freediscrim (DECRYPT K X) = freediscrim X - 2"
+primrec freediscrim :: "freemsg \<Rightarrow> int" where
+  "freediscrim (NONCE N) = 0"
+| "freediscrim (MPAIR X Y) = 1"
+| "freediscrim (CRYPT K X) = freediscrim X + 2"
+| "freediscrim (DECRYPT K X) = freediscrim X - 2"
 
 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
 theorem msgrel_imp_eq_freediscrim:
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -72,17 +72,14 @@
 be lifted to the initial algrebra, to serve as an example of that process.
 Note that the "free" refers to the free datatype rather than to the concept
 of a free variable.*}
-consts
-  freevars      :: "freeExp \<Rightarrow> nat set"
-  freevars_list :: "freeExp list \<Rightarrow> nat set"
+primrec freevars :: "freeExp \<Rightarrow> nat set" 
+  and freevars_list :: "freeExp list \<Rightarrow> nat set" where
+  "freevars (VAR N) = {N}"
+| "freevars (PLUS X Y) = freevars X \<union> freevars Y"
+| "freevars (FNCALL F Xs) = freevars_list Xs"
 
-primrec
-   "freevars (VAR N) = {N}"
-   "freevars (PLUS X Y) = freevars X \<union> freevars Y"
-   "freevars (FNCALL F Xs) = freevars_list Xs"
-
-   "freevars_list [] = {}"
-   "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
+| "freevars_list [] = {}"
+| "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
 
 text{*This theorem lets us prove that the vars function respects the
 equivalence relation.  It also helps us prove that Variable
@@ -98,11 +95,10 @@
 subsubsection{*Functions for Freeness*}
 
 text{*A discriminator function to distinguish vars, sums and function calls*}
-consts freediscrim :: "freeExp \<Rightarrow> int"
-primrec
-   "freediscrim (VAR N) = 0"
-   "freediscrim (PLUS X Y) = 1"
-   "freediscrim (FNCALL F Xs) = 2"
+primrec freediscrim :: "freeExp \<Rightarrow> int" where
+  "freediscrim (VAR N) = 0"
+| "freediscrim (PLUS X Y) = 1"
+| "freediscrim (FNCALL F Xs) = 2"
 
 theorem exprel_imp_eq_freediscrim:
      "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
@@ -111,12 +107,10 @@
 
 text{*This function, which returns the function name, is used to
 prove part of the injectivity property for FnCall.*}
-consts  freefun :: "freeExp \<Rightarrow> nat"
-
-primrec
-   "freefun (VAR N) = 0"
-   "freefun (PLUS X Y) = 0"
-   "freefun (FNCALL F Xs) = F"
+primrec freefun :: "freeExp \<Rightarrow> nat" where
+  "freefun (VAR N) = 0"
+| "freefun (PLUS X Y) = 0"
+| "freefun (FNCALL F Xs) = F"
 
 theorem exprel_imp_eq_freefun:
      "U \<sim> V \<Longrightarrow> freefun U = freefun V"
@@ -125,11 +119,10 @@
 
 text{*This function, which returns the list of function arguments, is used to
 prove part of the injectivity property for FnCall.*}
-consts  freeargs      :: "freeExp \<Rightarrow> freeExp list"
-primrec
-   "freeargs (VAR N) = []"
-   "freeargs (PLUS X Y) = []"
-   "freeargs (FNCALL F Xs) = Xs"
+primrec freeargs :: "freeExp \<Rightarrow> freeExp list" where
+  "freeargs (VAR N) = []"
+| "freeargs (PLUS X Y) = []"
+| "freeargs (FNCALL F Xs) = Xs"
 
 theorem exprel_imp_eqv_freeargs:
      "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
@@ -285,10 +278,9 @@
 by (simp add: congruent_def exprel_imp_eq_freevars) 
 
 text{*The extension of the function @{term vars} to lists*}
-consts vars_list :: "exp list \<Rightarrow> nat set"
-primrec
-   "vars_list []    = {}"
-   "vars_list(E#Es) = vars E \<union> vars_list Es"
+primrec vars_list :: "exp list \<Rightarrow> nat set" where
+  "vars_list []    = {}"
+| "vars_list(E#Es) = vars E \<union> vars_list Es"
 
 
 text{*Now prove the three equations for @{term vars}*}
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Induct/SList.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -133,10 +133,9 @@
   map       :: "('a=>'b) => ('a list => 'b list)" where
   "map f xs = list_rec xs [] (%x l r. f(x)#r)"
 
-consts take      :: "['a list,nat] => 'a list"
-primrec
+primrec take :: "['a list,nat] => 'a list" where
   take_0:  "take xs 0 = []"
-  take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
+| take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
 
 lemma ListI: "x : list (range Leaf) ==> x : List"
 by (simp add: List_def)
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Induct/Tree.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -95,15 +95,15 @@
 text{*Example of a general function*}
 
 function
-  add2 :: "(brouwer*brouwer) => brouwer"
+  add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
 where
-  "add2 (i, Zero) = i"
-| "add2 (i, (Succ j)) = Succ (add2 (i, j))"
-| "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
+  "add2 i Zero = i"
+| "add2 i (Succ j) = Succ (add2 i j)"
+| "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
 by pat_completeness auto
 termination by (relation "inv_image brouwer_order snd") auto
 
-lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
+lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
   by (induct k) auto
 
 end
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Lattice/Orders.thy
--- a/src/HOL/Lattice/Orders.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Lattice/Orders.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -48,9 +48,7 @@
 
 datatype 'a dual = dual 'a
 
-consts
-  undual :: "'a dual \<Rightarrow> 'a"
-primrec
+primrec undual :: "'a dual \<Rightarrow> 'a" where
   undual_dual: "undual (dual x) = x"
 
 instantiation dual :: (leq) leq
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Metis_Examples/BT.thy
--- a/src/HOL/Metis_Examples/BT.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -15,53 +15,41 @@
     Lf
   | Br 'a  "'a bt"  "'a bt"
 
-consts
-  n_nodes   :: "'a bt => nat"
-  n_leaves  :: "'a bt => nat"
-  depth     :: "'a bt => nat"
-  reflect   :: "'a bt => 'a bt"
-  bt_map    :: "('a => 'b) => ('a bt => 'b bt)"
-  preorder  :: "'a bt => 'a list"
-  inorder   :: "'a bt => 'a list"
-  postorder :: "'a bt => 'a list"
-  appnd    :: "'a bt => 'a bt => 'a bt"
+primrec n_nodes :: "'a bt => nat" where
+  "n_nodes Lf = 0"
+| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+
+primrec n_leaves :: "'a bt => nat" where
+  "n_leaves Lf = Suc 0"
+| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
 
-primrec
-  "n_nodes Lf = 0"
-  "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+primrec depth :: "'a bt => nat" where
+  "depth Lf = 0"
+| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
 
-primrec
-  "n_leaves Lf = Suc 0"
-  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-
-primrec
-  "depth Lf = 0"
-  "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
+primrec reflect :: "'a bt => 'a bt" where
+  "reflect Lf = Lf"
+| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
 
-primrec
-  "reflect Lf = Lf"
-  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-
-primrec
+primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
   "bt_map f Lf = Lf"
-  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
+| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
 
-primrec
+primrec preorder :: "'a bt => 'a list" where
   "preorder Lf = []"
-  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
 
-primrec
+primrec inorder :: "'a bt => 'a list" where
   "inorder Lf = []"
-  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
 
-primrec
+primrec postorder :: "'a bt => 'a list" where
   "postorder Lf = []"
-  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
 
-primrec
-  "appnd Lf t = t"
-  "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)"
-
+primrec append :: "'a bt => 'a bt => 'a bt" where
+  "append Lf t = t"
+| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
 
 text {* \medskip BT simplification *}
 
@@ -135,12 +123,12 @@
  apply (metis bt_map.simps(1))
 by (metis bt_map.simps(2))
 
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_appnd" ]]
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
 
-lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
+lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)"
 apply (induct t)
- apply (metis appnd.simps(1) bt_map.simps(1))
-by (metis appnd.simps(2) bt_map.simps(2))
+ apply (metis append.simps(1) bt_map.simps(1))
+by (metis append.simps(2) bt_map.simps(2))
 
 declare [[ sledgehammer_problem_prefix = "BT__bt_map_compose" ]]
 
@@ -219,8 +207,8 @@
 apply (induct t)
  apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
               reflect.simps(1))
-by (metis append.simps(1) append.simps(2) postorder.simps(2) preorder.simps(2)
-          reflect.simps(2) rev.simps(2) rev_append rev_swap)
+apply simp
+done
 
 declare [[ sledgehammer_problem_prefix = "BT__inorder_reflect" ]]
 
@@ -245,44 +233,44 @@
 Analogues of the standard properties of the append function for lists.
 *}
 
-declare [[ sledgehammer_problem_prefix = "BT__appnd_assoc" ]]
+declare [[ sledgehammer_problem_prefix = "BT__append_assoc" ]]
 
-lemma appnd_assoc [simp]: "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
+lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)"
 apply (induct t1)
- apply (metis appnd.simps(1))
-by (metis appnd.simps(2))
+ apply (metis append.simps(1))
+by (metis append.simps(2))
 
-declare [[ sledgehammer_problem_prefix = "BT__appnd_Lf2" ]]
+declare [[ sledgehammer_problem_prefix = "BT__append_Lf2" ]]
 
-lemma appnd_Lf2 [simp]: "appnd t Lf = t"
+lemma append_Lf2 [simp]: "append t Lf = t"
 apply (induct t)
- apply (metis appnd.simps(1))
-by (metis appnd.simps(2))
+ apply (metis append.simps(1))
+by (metis append.simps(2))
 
 declare max_add_distrib_left [simp]
 
-declare [[ sledgehammer_problem_prefix = "BT__depth_appnd" ]]
+declare [[ sledgehammer_problem_prefix = "BT__depth_append" ]]
 
-lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
+lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
 apply (induct t1)
- apply (metis appnd.simps(1) depth.simps(1) plus_nat.simps(1))
+ apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1))
 by simp
 
-declare [[ sledgehammer_problem_prefix = "BT__n_leaves_appnd" ]]
+declare [[ sledgehammer_problem_prefix = "BT__n_leaves_append" ]]
 
-lemma n_leaves_appnd [simp]:
-     "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
+lemma n_leaves_append [simp]:
+     "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
 apply (induct t1)
- apply (metis appnd.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
+ apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
               semiring_norm(111))
 by (simp add: left_distrib)
 
-declare [[ sledgehammer_problem_prefix = "BT__bt_map_appnd" ]]
+declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
 
-lemma (*bt_map_appnd:*)
-     "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
+lemma (*bt_map_append:*)
+     "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
 apply (induct t1)
- apply (metis appnd.simps(1) bt_map.simps(1))
-by (metis bt_map_appnd)
+ apply (metis append.simps(1) bt_map.simps(1))
+by (metis bt_map_append)
 
 end
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Nominal/Examples/Class3.thy
--- a/src/HOL/Nominal/Examples/Class3.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Nominal/Examples/Class3.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -5956,17 +5956,13 @@
     done
 qed
 
-consts
-  "idn" :: "(name\<times>ty) list\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list"
-primrec
+primrec "idn" :: "(name\<times>ty) list\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list" where
   "idn [] a   = []"
-  "idn (p#\<Gamma>) a = ((fst p),a,Ax (fst p) a)#(idn \<Gamma> a)"
-
-consts
-  "idc" :: "(coname\<times>ty) list\<Rightarrow>name\<Rightarrow>(coname\<times>name\<times>trm) list"
-primrec
+| "idn (p#\<Gamma>) a = ((fst p),a,Ax (fst p) a)#(idn \<Gamma> a)"
+
+primrec "idc" :: "(coname\<times>ty) list\<Rightarrow>name\<Rightarrow>(coname\<times>name\<times>trm) list" where
   "idc [] x    = []"
-  "idc (p#\<Delta>) x = ((fst p),x,Ax x (fst p))#(idc \<Delta> x)"
+| "idc (p#\<Delta>) x = ((fst p),x,Ax x (fst p))#(idc \<Delta> x)"
 
 lemma idn_eqvt[eqvt]:
   fixes pi1::"name prm"
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -107,17 +107,17 @@
 | "vrs_of (TVarB x y) = {}"
 by auto
 
-consts
+primrec
   "ty_dom" :: "env \<Rightarrow> tyvrs set"
-primrec
+where
   "ty_dom [] = {}"
-  "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)" 
+| "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)" 
 
-consts
+primrec
   "trm_dom" :: "env \<Rightarrow> vrs set"
-primrec
+where
   "trm_dom [] = {}"
-  "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)" 
+| "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)" 
 
 lemma vrs_of_eqvt[eqvt]:
   fixes pi ::"tyvrs prm"
@@ -475,12 +475,9 @@
 by (induct B rule: binding.induct)
    (simp_all add: fresh_atm type_subst_identity)
 
-consts 
-  subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100)
-
-primrec
-"([])[Y \<mapsto> T]\<^sub>e= []"
-"(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
+primrec subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100) where
+  "([])[Y \<mapsto> T]\<^sub>e= []"
+| "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
 
 lemma ctxt_subst_fresh':
   fixes X::"tyvrs"
@@ -686,13 +683,13 @@
   have fresh_cond: "X\<sharp>\<Gamma>" by fact
   hence fresh_ty_dom: "X\<sharp>(ty_dom \<Gamma>)" by (simp add: fresh_dom)
   have "(\<forall>X<:T\<^isub>2. T\<^isub>1) closed_in \<Gamma>" by fact
-  hence closed\<^isub>T\<^isub>2: "T\<^isub>2 closed_in \<Gamma>" and closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in ((TVarB  X T\<^isub>2)#\<Gamma>)" 
+  hence closed\<^isub>T2: "T\<^isub>2 closed_in \<Gamma>" and closed\<^isub>T1: "T\<^isub>1 closed_in ((TVarB  X T\<^isub>2)#\<Gamma>)" 
     by (auto simp add: closed_in_def ty.supp abs_supp)
   have ok: "\<turnstile> \<Gamma> ok" by fact  
-  hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_ty_dom by simp
-  have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp
+  hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T2 fresh_ty_dom by simp
+  have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T2 ok by simp
   moreover
-  have "((TVarB X T\<^isub>2)#\<Gamma>) \<turnstile> T\<^isub>1 <: T\<^isub>1" using ih_T\<^isub>1 closed\<^isub>T\<^isub>1 ok' by simp
+  have "((TVarB X T\<^isub>2)#\<Gamma>) \<turnstile> T\<^isub>1 <: T\<^isub>1" using ih_T\<^isub>1 closed\<^isub>T1 ok' by simp
   ultimately show "\<Gamma> \<turnstile> (\<forall>X<:T\<^isub>2. T\<^isub>1) <: (\<forall>X<:T\<^isub>2. T\<^isub>1)" using fresh_cond 
     by (simp add: subtype_of.SA_all)
 qed (auto simp add: closed_in_def ty.supp supp_atm)
@@ -783,10 +780,10 @@
   have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
   have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
-  hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
+  hence closed\<^isub>T1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   have ok: "\<turnstile> \<Delta> ok" by fact
   have ext: "\<Delta> extends \<Gamma>" by fact
-  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
+  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T1 by (simp only: extends_closed)
   hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force   
   moreover 
   have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
@@ -811,10 +808,10 @@
   have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
   have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
   have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
-  hence closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
+  hence closed\<^isub>T1: "T\<^isub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   have ok: "\<turnstile> \<Delta> ok" by fact
   have ext: "\<Delta> extends \<Gamma>" by fact
-  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
+  have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T1 by (simp only: extends_closed)
   hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force   
   moreover
   have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
@@ -903,7 +900,7 @@
       case (SA_arrow \<Gamma> Q\<^isub>1 S\<^isub>1 S\<^isub>2 Q\<^isub>2) 
       then have rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp
       from `Q\<^isub>1 \<rightarrow> Q\<^isub>2 = Q` 
-      have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto
+      have Q\<^isub>12_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto
       have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
       have lh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact      
       from rh_drv have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2)" 
@@ -921,10 +918,10 @@
           and   rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1"
           and   rh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
         from IH_trans[of "Q\<^isub>1"] 
-        have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>1 lh_drv_prm\<^isub>1 by simp 
+        have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using Q\<^isub>12_less rh_drv_prm\<^isub>1 lh_drv_prm\<^isub>1 by simp 
         moreover
         from IH_trans[of "Q\<^isub>2"] 
-        have "\<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 lh_drv_prm\<^isub>2 by simp
+        have "\<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>12_less rh_drv_prm\<^isub>2 lh_drv_prm\<^isub>2 by simp
         ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
         then have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp
       }
@@ -954,15 +951,15 @@
           and   rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1" 
           and   rh_drv_prm\<^isub>2:"((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
         have "(\<forall>X<:Q\<^isub>1. Q\<^isub>2) = Q" by fact 
-        then have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" 
+        then have Q\<^isub>12_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" 
           using fresh_cond by auto
         from IH_trans[of "Q\<^isub>1"] 
-        have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using lh_drv_prm\<^isub>1 rh_drv_prm\<^isub>1 Q\<^isub>1\<^isub>2_less by blast
+        have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using lh_drv_prm\<^isub>1 rh_drv_prm\<^isub>1 Q\<^isub>12_less by blast
         moreover
         from IH_narrow[of "Q\<^isub>1" "[]"] 
-        have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" using Q\<^isub>1\<^isub>2_less lh_drv_prm\<^isub>2 rh_drv_prm\<^isub>1 by simp
+        have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" using Q\<^isub>12_less lh_drv_prm\<^isub>2 rh_drv_prm\<^isub>1 by simp
         with IH_trans[of "Q\<^isub>2"] 
-        have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 by simp
+        have "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>12_less rh_drv_prm\<^isub>2 by simp
         ultimately have "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)"
           using fresh_cond by (simp add: subtype_of.SA_all)
         hence "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T" using T_inst by simp
@@ -1005,16 +1002,16 @@
         with IH_inner show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" by (simp add: subtype_of.SA_trans_TVar)
       next
         case True
-        have memb\<^isub>X\<^isub>Q: "(TVarB X Q)\<in>set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp
-        have memb\<^isub>X\<^isub>P: "(TVarB X P)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" by simp
+        have memb\<^isub>XQ: "(TVarB X Q)\<in>set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp
+        have memb\<^isub>XP: "(TVarB X P)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" by simp
         have eq: "X=Y" by fact 
-        hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>X\<^isub>Q by (simp only: uniqueness_of_ctxt)
+        hence "S=Q" using ok\<^isub>Q lh_drv_prm memb\<^isub>XQ by (simp only: uniqueness_of_ctxt)
         hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp
         moreover
         have "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
         hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^isub>P by (simp only: weakening)
         ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_lemma) 
-        then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto
+        then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>XP eq by auto
       qed
     next
       case (SA_refl_TVar Y \<Gamma> X \<Delta>)
@@ -1049,7 +1046,7 @@
 | T_Abs[intro]: "\<lbrakk> VarB x T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> T\<^isub>2"
 | T_Sub[intro]: "\<lbrakk> \<Gamma> \<turnstile> t : S; \<Gamma> \<turnstile> S <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t : T"
 | T_TAbs[intro]:"\<lbrakk> TVarB X T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>1. t\<^isub>2) : (\<forall>X<:T\<^isub>1. T\<^isub>2)"
-| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^isub>1,T\<^isub>2); \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2); \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 : (T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>)" 
+| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^isub>1,T\<^isub>2); \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T\<^isub>11. T\<^isub>12); \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 : (T\<^isub>12[X \<mapsto> T\<^isub>2]\<^sub>\<tau>)" 
 
 equivariance typing
 
@@ -1164,10 +1161,10 @@
 inductive 
   eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60)
 where
-  E_Abs         : "\<lbrakk> x \<sharp> v\<^isub>2; val v\<^isub>2 \<rbrakk> \<Longrightarrow> (\<lambda>x:T\<^isub>1\<^isub>1. t\<^isub>1\<^isub>2) \<cdot> v\<^isub>2 \<longmapsto> t\<^isub>1\<^isub>2[x \<mapsto> v\<^isub>2]"
+  E_Abs         : "\<lbrakk> x \<sharp> v\<^isub>2; val v\<^isub>2 \<rbrakk> \<Longrightarrow> (\<lambda>x:T\<^isub>11. t\<^isub>12) \<cdot> v\<^isub>2 \<longmapsto> t\<^isub>12[x \<mapsto> v\<^isub>2]"
 | E_App1 [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
 | E_App2 [intro]: "\<lbrakk> val v; t \<longmapsto> t' \<rbrakk> \<Longrightarrow> v \<cdot> t \<longmapsto> v \<cdot> t'"
-| E_TAbs        : "X \<sharp> (T\<^isub>1\<^isub>1, T\<^isub>2) \<Longrightarrow> (\<lambda>X<:T\<^isub>1\<^isub>1. t\<^isub>1\<^isub>2) \<cdot>\<^sub>\<tau> T\<^isub>2 \<longmapsto> t\<^isub>1\<^isub>2[X \<mapsto>\<^sub>\<tau> T\<^isub>2]"
+| E_TAbs        : "X \<sharp> (T\<^isub>11, T\<^isub>2) \<Longrightarrow> (\<lambda>X<:T\<^isub>11. t\<^isub>12) \<cdot>\<^sub>\<tau> T\<^isub>2 \<longmapsto> t\<^isub>12[X \<mapsto>\<^sub>\<tau> T\<^isub>2]"
 | E_TApp [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot>\<^sub>\<tau> T \<longmapsto> t' \<cdot>\<^sub>\<tau> T"
 
 lemma better_E_Abs[intro]:
@@ -1315,7 +1312,7 @@
   case (T_Var x T)
   then show ?case by auto
 next
-  case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
+  case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>11 T\<^isub>12)
   then show ?case by force
 next
   case (T_Abs y T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
@@ -1744,68 +1741,68 @@
   assumes H: "\<Gamma> \<turnstile> t : T"
   shows "t \<longmapsto> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : T" using H
 proof (nominal_induct avoiding: t' rule: typing.strong_induct)
-  case (T_App \<Gamma> t\<^isub>1 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2 t\<^isub>2 t')
+  case (T_App \<Gamma> t\<^isub>1 T\<^isub>11 T\<^isub>12 t\<^isub>2 t')
   obtain x::vrs where x_fresh: "x \<sharp> (\<Gamma>, t\<^isub>1 \<cdot> t\<^isub>2, t')"
     by (rule exists_fresh) (rule fin_supp)
   obtain X::tyvrs where "X \<sharp> (t\<^isub>1 \<cdot> t\<^isub>2, t')"
     by (rule exists_fresh) (rule fin_supp)
   with `t\<^isub>1 \<cdot> t\<^isub>2 \<longmapsto> t'` show ?case
   proof (cases rule: eval.strong_cases [where x=x and X=X])
-    case (E_Abs v\<^isub>2 T\<^isub>1\<^isub>1' t\<^isub>1\<^isub>2)
-    with T_App and x_fresh have h: "\<Gamma> \<turnstile> (\<lambda>x:T\<^isub>1\<^isub>1'. t\<^isub>1\<^isub>2) : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2"
+    case (E_Abs v\<^isub>2 T\<^isub>11' t\<^isub>12)
+    with T_App and x_fresh have h: "\<Gamma> \<turnstile> (\<lambda>x:T\<^isub>11'. t\<^isub>12) : T\<^isub>11 \<rightarrow> T\<^isub>12"
       by (simp add: trm.inject fresh_prod)
     moreover from x_fresh have "x \<sharp> \<Gamma>" by simp
     ultimately obtain S'
-      where T\<^isub>1\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1\<^isub>1 <: T\<^isub>1\<^isub>1'"
-      and t\<^isub>1\<^isub>2: "(VarB x T\<^isub>1\<^isub>1') # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : S'"
-      and S': "\<Gamma> \<turnstile> S' <: T\<^isub>1\<^isub>2"
+      where T\<^isub>11: "\<Gamma> \<turnstile> T\<^isub>11 <: T\<^isub>11'"
+      and t\<^isub>12: "(VarB x T\<^isub>11') # \<Gamma> \<turnstile> t\<^isub>12 : S'"
+      and S': "\<Gamma> \<turnstile> S' <: T\<^isub>12"
       by (rule Abs_type') blast
-    from `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1`
-    have "\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1'" using T\<^isub>1\<^isub>1 by (rule T_Sub)
-    with t\<^isub>1\<^isub>2 have "\<Gamma> \<turnstile> t\<^isub>1\<^isub>2[x \<mapsto> t\<^isub>2] : S'" 
+    from `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11`
+    have "\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11'" using T\<^isub>11 by (rule T_Sub)
+    with t\<^isub>12 have "\<Gamma> \<turnstile> t\<^isub>12[x \<mapsto> t\<^isub>2] : S'" 
       by (rule subst_type [where \<Delta>="[]", simplified])
-    hence "\<Gamma> \<turnstile> t\<^isub>1\<^isub>2[x \<mapsto> t\<^isub>2] : T\<^isub>1\<^isub>2" using S' by (rule T_Sub)
+    hence "\<Gamma> \<turnstile> t\<^isub>12[x \<mapsto> t\<^isub>2] : T\<^isub>12" using S' by (rule T_Sub)
     with E_Abs and x_fresh show ?thesis by (simp add: trm.inject fresh_prod)
   next
     case (E_App1 t''' t'' u)
     hence "t\<^isub>1 \<longmapsto> t''" by (simp add:trm.inject) 
-    hence "\<Gamma> \<turnstile> t'' : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2" by (rule T_App)
-    hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^isub>2 : T\<^isub>1\<^isub>2" using `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1`
+    hence "\<Gamma> \<turnstile> t'' : T\<^isub>11 \<rightarrow> T\<^isub>12" by (rule T_App)
+    hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^isub>2 : T\<^isub>12" using `\<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11`
       by (rule typing.T_App)
     with E_App1 show ?thesis by (simp add:trm.inject)
   next
     case (E_App2 v t''' t'')
     hence "t\<^isub>2 \<longmapsto> t''" by (simp add:trm.inject) 
-    hence "\<Gamma> \<turnstile> t'' : T\<^isub>1\<^isub>1" by (rule T_App)
-    with T_App(1) have "\<Gamma> \<turnstile> t\<^isub>1 \<cdot> t'' : T\<^isub>1\<^isub>2"
+    hence "\<Gamma> \<turnstile> t'' : T\<^isub>11" by (rule T_App)
+    with T_App(1) have "\<Gamma> \<turnstile> t\<^isub>1 \<cdot> t'' : T\<^isub>12"
       by (rule typing.T_App)
     with E_App2 show ?thesis by (simp add:trm.inject) 
   qed (simp_all add: fresh_prod)
 next
-  case (T_TApp X \<Gamma> t\<^isub>1 T\<^isub>2  T\<^isub>1\<^isub>1  T\<^isub>1\<^isub>2 t')
+  case (T_TApp X \<Gamma> t\<^isub>1 T\<^isub>2  T\<^isub>11  T\<^isub>12 t')
   obtain x::vrs where "x \<sharp> (t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2, t')"
     by (rule exists_fresh) (rule fin_supp)
   with `t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 \<longmapsto> t'`
   show ?case
   proof (cases rule: eval.strong_cases [where X=X and x=x])
-    case (E_TAbs T\<^isub>1\<^isub>1' T\<^isub>2' t\<^isub>1\<^isub>2)
-    with T_TApp have "\<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>1\<^isub>1'. t\<^isub>1\<^isub>2) : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2)" and "X \<sharp> \<Gamma>" and "X \<sharp> T\<^isub>1\<^isub>1'"
+    case (E_TAbs T\<^isub>11' T\<^isub>2' t\<^isub>12)
+    with T_TApp have "\<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>11'. t\<^isub>12) : (\<forall>X<:T\<^isub>11. T\<^isub>12)" and "X \<sharp> \<Gamma>" and "X \<sharp> T\<^isub>11'"
       by (simp_all add: trm.inject)
-    moreover from `\<Gamma>\<turnstile>T\<^isub>2<:T\<^isub>1\<^isub>1` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^isub>1\<^isub>1"
+    moreover from `\<Gamma>\<turnstile>T\<^isub>2<:T\<^isub>11` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^isub>11"
       by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed)
     ultimately obtain S'
-      where "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : S'"
-      and "(TVarB X T\<^isub>1\<^isub>1 # \<Gamma>) \<turnstile> S' <: T\<^isub>1\<^isub>2"
+      where "TVarB X T\<^isub>11 # \<Gamma> \<turnstile> t\<^isub>12 : S'"
+      and "(TVarB X T\<^isub>11 # \<Gamma>) \<turnstile> S' <: T\<^isub>12"
       by (rule TAbs_type') blast
-    hence "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : T\<^isub>1\<^isub>2" by (rule T_Sub)
-    hence "\<Gamma> \<turnstile> t\<^isub>1\<^isub>2[X \<mapsto>\<^sub>\<tau> T\<^isub>2] : T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>" using `\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1`
+    hence "TVarB X T\<^isub>11 # \<Gamma> \<turnstile> t\<^isub>12 : T\<^isub>12" by (rule T_Sub)
+    hence "\<Gamma> \<turnstile> t\<^isub>12[X \<mapsto>\<^sub>\<tau> T\<^isub>2] : T\<^isub>12[X \<mapsto> T\<^isub>2]\<^sub>\<tau>" using `\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11`
       by (rule substT_type [where D="[]", simplified])
     with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject)
   next
     case (E_TApp t''' t'' T)
     from E_TApp have "t\<^isub>1 \<longmapsto> t''" by (simp add: trm.inject)
-    then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2)" by (rule T_TApp)
-    then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>" using `\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1`
+    then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^isub>11. T\<^isub>12)" by (rule T_TApp)
+    then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^isub>2 : T\<^isub>12[X \<mapsto> T\<^isub>2]\<^sub>\<tau>" using `\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11`
       by (rule better_T_TApp)
     with E_TApp show ?thesis by (simp add: trm.inject)
   qed (simp_all add: fresh_prod)
@@ -1845,7 +1842,7 @@
   shows "val t \<or> (\<exists>t'. t \<longmapsto> t')" 
 using assms
 proof (induct "[]::env" t T)
-  case (T_App t\<^isub>1 T\<^isub>1\<^isub>1  T\<^isub>1\<^isub>2 t\<^isub>2)
+  case (T_App t\<^isub>1 T\<^isub>11  T\<^isub>12 t\<^isub>2)
   hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
   thus ?case
   proof
@@ -1871,7 +1868,7 @@
     thus ?case by auto
   qed
 next
-  case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
+  case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>11 T\<^isub>12)
   hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
   thus ?case
   proof
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/Nominal/Examples/W.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -150,12 +150,9 @@
 equivariance valid
 
 text {* General *}
-consts
-  gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS"
-
-primrec 
+primrec gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS" where
   "gen T [] = Ty T"
-  "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
+| "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
 
 lemma gen_eqvt[eqvt]:
   fixes pi::"tvar prm"
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -15,17 +15,11 @@
   NbT_pos:  "0 < NbT"
 
 (*This function merely sums the elements of a list*)
-consts tokens     :: "nat list => nat"
-primrec 
+primrec tokens :: "nat list => nat" where
   "tokens [] = 0"
-  "tokens (x#xs) = x + tokens xs"
+| "tokens (x#xs) = x + tokens xs"
 
-consts
-  bag_of :: "'a list => 'a multiset"
-
-primrec
-  "bag_of []     = {#}"
-  "bag_of (x#xs) = {#x#} + bag_of xs"
+abbreviation (input) "bag_of \<equiv> multiset_of"
 
 lemma setsum_fun_mono [rule_format]:
      "!!f :: nat=>nat.  
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -402,12 +402,9 @@
     done
 qed
 
-consts
-  nat2Nat :: "nat \<Rightarrow> ZF"
-
-primrec
-nat2Nat_0[intro]:  "nat2Nat 0 = Empty"
-nat2Nat_Suc[intro]:  "nat2Nat (Suc n) = SucNat (nat2Nat n)"
+primrec nat2Nat :: "nat \<Rightarrow> ZF" where
+  nat2Nat_0[intro]:  "nat2Nat 0 = Empty"
+| nat2Nat_Suc[intro]:  "nat2Nat (Suc n) = SucNat (nat2Nat n)"
 
 definition Nat2nat :: "ZF \<Rightarrow> nat" where
   "Nat2nat == inv nat2Nat"
@@ -500,12 +497,9 @@
   apply auto
   done
 
-consts
-  NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF"
-
-primrec
+primrec NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF" where
   "NatInterval n 0 = Singleton (nat2Nat n)"
-  "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))"
+| "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))"
 
 lemma n_Elem_NatInterval[rule_format]: "! q. q <= m \<longrightarrow> Elem (nat2Nat (n+q)) (NatInterval n m)"
   apply (induct m)
@@ -729,12 +723,9 @@
   apply (simp add: Ext_def)
   done
 
-consts
-  Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF"
-
-primrec
+primrec Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF" where
   "Ext_ZF_n R s 0 = Ext_ZF R s"
-  "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))"
+| "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))"
 
 definition Ext_ZF_hull :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF" where
   "Ext_ZF_hull R s == SeqSum (Ext_ZF_n R s)"
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/ex/BT.thy
--- a/src/HOL/ex/BT.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/ex/BT.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/BT.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
@@ -14,53 +13,41 @@
     Lf
   | Br 'a  "'a bt"  "'a bt"
 
-consts
-  n_nodes   :: "'a bt => nat"
-  n_leaves  :: "'a bt => nat"
-  depth     :: "'a bt => nat"
-  reflect   :: "'a bt => 'a bt"
-  bt_map    :: "('a => 'b) => ('a bt => 'b bt)"
-  preorder  :: "'a bt => 'a list"
-  inorder   :: "'a bt => 'a list"
-  postorder :: "'a bt => 'a list"
-  append     :: "'a bt => 'a bt => 'a bt"
+primrec n_nodes :: "'a bt => nat" where
+  "n_nodes Lf = 0"
+| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+
+primrec n_leaves :: "'a bt => nat" where
+  "n_leaves Lf = Suc 0"
+| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
 
-primrec
-  "n_nodes Lf = 0"
-  "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
+primrec depth :: "'a bt => nat" where
+  "depth Lf = 0"
+| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
 
-primrec
-  "n_leaves Lf = Suc 0"
-  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-
-primrec
-  "depth Lf = 0"
-  "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
+primrec reflect :: "'a bt => 'a bt" where
+  "reflect Lf = Lf"
+| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
 
-primrec
-  "reflect Lf = Lf"
-  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-
-primrec
+primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
   "bt_map f Lf = Lf"
-  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
+| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
 
-primrec
+primrec preorder :: "'a bt => 'a list" where
   "preorder Lf = []"
-  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
 
-primrec
+primrec inorder :: "'a bt => 'a list" where
   "inorder Lf = []"
-  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
 
-primrec
+primrec postorder :: "'a bt => 'a list" where
   "postorder Lf = []"
-  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
 
-primrec
+primrec append :: "'a bt => 'a bt => 'a bt" where
   "append Lf t = t"
-  "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
-
+| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
 
 text {* \medskip BT simplification *}
 
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/ex/Chinese.thy
--- a/src/HOL/ex/Chinese.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/ex/Chinese.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -1,5 +1,4 @@
 (* -*- coding: utf-8 -*- :encoding=utf-8:
-    ID:         $Id$
     Author:     Ning Zhang and Christian Urban
 
 Example theory involving Unicode characters (UTF-8 encoding) -- both
@@ -30,20 +29,17 @@
   | Nine  ("九")
   | Ten   ("十")
 
-consts
-  translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100)
-
-primrec
+primrec translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100) where
  "|一| = 1"
- "|二| = 2"
- "|三| = 3"
- "|四| = 4"
- "|五| = 5"
- "|六| = 6"
- "|七| = 7"
- "|八| = 8"
- "|九| = 9"
- "|十| = 10"
+|"|二| = 2"
+|"|三| = 3"
+|"|四| = 4"
+|"|五| = 5"
+|"|六| = 6"
+|"|七| = 7"
+|"|八| = 8"
+|"|九| = 9"
+|"|十| = 10"
 
 thm translate.simps
 
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/ex/Hebrew.thy
--- a/src/HOL/ex/Hebrew.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/ex/Hebrew.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -1,5 +1,4 @@
 (* -*- coding: utf-8 -*- :encoding=utf-8:  
-    ID:         $Id$
     Author:     Makarius
 
 Example theory involving Unicode characters (UTF-8 encoding) -- both
@@ -43,31 +42,29 @@
 
 text {* Interpreting Hebrew letters as numbers. *}
 
-consts
-  mispar :: "alef_bet => nat"
-primrec
+primrec mispar :: "alef_bet => nat" where
   "mispar א = 1"
-  "mispar ב = 2"
-  "mispar ג = 3"
-  "mispar ד = 4"
-  "mispar ה = 5"
-  "mispar ו = 6"
-  "mispar ז = 7"
-  "mispar ח = 8"
-  "mispar ט = 9"
-  "mispar י = 10"
-  "mispar כ = 20"
-  "mispar ל = 30"
-  "mispar מ = 40"
-  "mispar נ = 50"
-  "mispar ס = 60"
-  "mispar ע = 70"
-  "mispar פ = 80"
-  "mispar צ = 90"
-  "mispar ק = 100"
-  "mispar ר = 200"
-  "mispar ש = 300"
-  "mispar ת = 400"
+| "mispar ב = 2"
+| "mispar ג = 3"
+| "mispar ד = 4"
+| "mispar ה = 5"
+| "mispar ו = 6"
+| "mispar ז = 7"
+| "mispar ח = 8"
+| "mispar ט = 9"
+| "mispar י = 10"
+| "mispar כ = 20"
+| "mispar ל = 30"
+| "mispar מ = 40"
+| "mispar נ = 50"
+| "mispar ס = 60"
+| "mispar ע = 70"
+| "mispar פ = 80"
+| "mispar צ = 90"
+| "mispar ק = 100"
+| "mispar ר = 200"
+| "mispar ש = 300"
+| "mispar ת = 400"
 
 thm mispar.simps
 
diff -r 5a3bd2b7d0ee -r 3a15ee47c610 src/HOL/ex/ReflectionEx.thy
--- a/src/HOL/ex/ReflectionEx.thy	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/HOL/ex/ReflectionEx.thy	Wed Sep 08 19:23:23 2010 +0200
@@ -46,14 +46,13 @@
 
 datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
 
-consts Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
-primrec
+primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool" where
   "Ifm (At n) vs = vs!n"
-  "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
-  "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
-  "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
-  "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
-  "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
+| "Ifm (And p q) vs = (Ifm p vs \<and> Ifm q vs)"
+| "Ifm (Or p q) vs = (Ifm p vs \<or> Ifm q vs)"
+| "Ifm (Imp p q) vs = (Ifm p vs \<longrightarrow> Ifm q vs)"
+| "Ifm (Iff p q) vs = (Ifm p vs = Ifm q vs)"
+| "Ifm (NOT p) vs = (\<not> (Ifm p vs))"
 
 lemma "Q \<longrightarrow> (D & F & ((~ D) & (~ F)))"
 apply (reify Ifm.simps)
@@ -399,7 +398,7 @@
 | "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)"
 | "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)"
 | "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs"
-consts prodmul:: "prod \<times> prod \<Rightarrow> prod"
+
 datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
   | Or sgn sgn | And sgn sgn