`code func` now just `code`
authorhaftmann
Fri Oct 10 06:45:53 2008 +0200 (2008-10-10)
changeset 285624e74209f113e
parent 28561 056255ade52a
child 28563 21b3a00a3ff0
`code func` now just `code`
doc-src/IsarAdvanced/Codegen/Thy/Program.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
src/HOL/Code_Eval.thy
src/HOL/Code_Setup.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/Equiv_Relations.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/Lattices.thy
src/HOL/Library/Array.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Char_chr.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Code_Message.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Enum.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Heap_Monad.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/RType.thy
src/HOL/Library/Ref.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/SparseMatrix.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HLim.thy
src/HOL/NSA/HLog.thy
src/HOL/NSA/HSEQ.thy
src/HOL/NSA/HSeries.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/HyperNat.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/NSCA.thy
src/HOL/NSA/NSComplex.thy
src/HOL/NSA/Star.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/NatBin.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Real/ContNotDenum.thy
src/HOL/Real/PReal.thy
src/HOL/Real/RComplete.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealVector.thy
src/HOL/Set.thy
src/HOL/SizeChange/Graphs.thy
src/HOL/SizeChange/Implementation.thy
src/HOL/Tools/ComputeHOL.thy
src/HOL/Wellfounded.thy
src/HOL/Word/BinGeneral.thy
src/HOL/Word/BinOperations.thy
src/HOL/Word/WordDefinition.thy
src/HOL/ex/Codegenerator_Pretty.thy
src/HOL/ex/NormalForm.thy
src/HOL/ex/Numeral.thy
src/HOL/ex/Random.thy
src/Pure/Isar/code.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    explicitly:
     1.5  *}
     1.6  
     1.7 -lemma %quoteme [code func]:
     1.8 +lemma %quoteme [code]:
     1.9    "dequeue (Queue xs []) =
    1.10       (if xs = [] then (None, Queue [] [])
    1.11         else dequeue (Queue [] (rev xs)))"
    1.12 @@ -34,7 +34,7 @@
    1.13    by (cases xs, simp_all) (cases "rev xs", simp_all)
    1.14  
    1.15  text {*
    1.16 -  \noindent The annotation @{text "[code func]"} is an @{text Isar}
    1.17 +  \noindent The annotation @{text "[code]"} is an @{text Isar}
    1.18    @{text attribute} which states that the given theorems should be
    1.19    considered as defining equations for a @{text fun} statement --
    1.20    the corresponding constant is determined syntactically.  The resulting code:
    1.21 @@ -255,7 +255,7 @@
    1.22    the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
    1.23  *}
    1.24  
    1.25 -lemma %quoteme plus_Dig [code func]:
    1.26 +lemma %quoteme plus_Dig [code]:
    1.27    "0 + n = n"
    1.28    "m + 0 = m"
    1.29    "1 + Dig0 n = Dig1 n"
    1.30 @@ -282,12 +282,12 @@
    1.31    which are an obstacle here:
    1.32  *}
    1.33  
    1.34 -lemma %quoteme Suc_Dig [code func]:
    1.35 +lemma %quoteme Suc_Dig [code]:
    1.36    "Suc n = n + 1"
    1.37    by simp
    1.38  
    1.39  declare %quoteme One_nat_def [code inline del]
    1.40 -declare %quoteme add_Suc_shift [code func del] 
    1.41 +declare %quoteme add_Suc_shift [code del] 
    1.42  
    1.43  text {*
    1.44    \noindent This yields the following code:
    1.45 @@ -316,10 +316,10 @@
    1.46  *}
    1.47  
    1.48  code_datatype %invisible "0::nat" Suc
    1.49 -declare %invisible plus_Dig [code func del]
    1.50 +declare %invisible plus_Dig [code del]
    1.51  declare %invisible One_nat_def [code inline]
    1.52 -declare %invisible add_Suc_shift [code func] 
    1.53 -lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
    1.54 +declare %invisible add_Suc_shift [code] 
    1.55 +lemma %invisible [code]: "0 + n = (n \<Colon> nat)" by simp
    1.56  
    1.57  
    1.58  subsection {* Equality and wellsortedness *}
    1.59 @@ -367,10 +367,10 @@
    1.60  instantiation %quoteme "*" :: (order, order) order
    1.61  begin
    1.62  
    1.63 -definition %quoteme [code func del]:
    1.64 +definition %quoteme [code del]:
    1.65    "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
    1.66  
    1.67 -definition %quoteme [code func del]:
    1.68 +definition %quoteme [code del]:
    1.69    "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
    1.70  
    1.71  instance %quoteme proof
    1.72 @@ -378,7 +378,7 @@
    1.73  
    1.74  end %quoteme
    1.75  
    1.76 -lemma %quoteme order_prod [code func]:
    1.77 +lemma %quoteme order_prod [code]:
    1.78    "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
    1.79       x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
    1.80    "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
    1.81 @@ -396,7 +396,7 @@
    1.82    code theorems:
    1.83  *}
    1.84  
    1.85 -lemma %quoteme order_prod_code [code func]:
    1.86 +lemma %quoteme order_prod_code [code]:
    1.87    "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
    1.88       x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
    1.89    "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
    1.90 @@ -438,7 +438,7 @@
    1.91    @{const [show_types] list_all2} can do the job:
    1.92  *}
    1.93  
    1.94 -lemma %quoteme monotype_eq_list_all2 [code func]:
    1.95 +lemma %quoteme monotype_eq_list_all2 [code]:
    1.96    "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
    1.97       eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
    1.98    by (simp add: eq list_all2_eq [symmetric])
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Fri Oct 10 06:45:50 2008 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Fri Oct 10 06:45:53 2008 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4  %
     2.5  \isatagquoteme
     2.6  \isacommand{lemma}\isamarkupfalse%
     2.7 -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
     2.8 +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
     2.9  \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
    2.10  \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
    2.11  \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.12 @@ -71,7 +71,7 @@
    2.13  \endisadelimquoteme
    2.14  %
    2.15  \begin{isamarkuptext}%
    2.16 -\noindent The annotation \isa{{\isacharbrackleft}code\ func{\isacharbrackright}} is an \isa{Isar}
    2.17 +\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
    2.18    \isa{attribute} which states that the given theorems should be
    2.19    considered as defining equations for a \isa{fun} statement --
    2.20    the corresponding constant is determined syntactically.  The resulting code:%
    2.21 @@ -287,8 +287,8 @@
    2.22  \verb|};|\newline%
    2.23  \newline%
    2.24  \verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
    2.25 +\verb|pow Zero_nat a = neutral;|\newline%
    2.26  \verb|pow (Suc n) a = mult a (pow n a);|\newline%
    2.27 -\verb|pow Zero_nat a = neutral;|\newline%
    2.28  \newline%
    2.29  \verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
    2.30  \verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
    2.31 @@ -298,8 +298,8 @@
    2.32  \verb|neutral_nat = Suc Zero_nat;|\newline%
    2.33  \newline%
    2.34  \verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
    2.35 +\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
    2.36  \verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
    2.37 -\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
    2.38  \newline%
    2.39  \verb|instance Semigroup Nat where {|\newline%
    2.40  \verb|  mult = mult_nat;|\newline%
    2.41 @@ -350,16 +350,16 @@
    2.42  \verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
    2.43  \verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
    2.44  \newline%
    2.45 -\verb|fun pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a)|\newline%
    2.46 -\verb|  |\verb,|,\verb| pow A_ Zero_nat a = neutral A_;|\newline%
    2.47 +\verb|fun pow A_ Zero_nat a = neutral A_|\newline%
    2.48 +\verb|  |\verb,|,\verb| pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a);|\newline%
    2.49  \newline%
    2.50  \verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
    2.51  \verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
    2.52  \newline%
    2.53  \verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
    2.54  \newline%
    2.55 -\verb|fun mult_nat (Suc m) n = plus_nat n (mult_nat m n)|\newline%
    2.56 -\verb|  |\verb,|,\verb| mult_nat Zero_nat n = Zero_nat;|\newline%
    2.57 +\verb|fun mult_nat Zero_nat n = Zero_nat|\newline%
    2.58 +\verb|  |\verb,|,\verb| mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
    2.59  \newline%
    2.60  \verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
    2.61  \newline%
    2.62 @@ -575,7 +575,7 @@
    2.63  %
    2.64  \isatagquoteme
    2.65  \isacommand{lemma}\isamarkupfalse%
    2.66 -\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
    2.67 +\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
    2.68  \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
    2.69  \ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
    2.70  \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
    2.71 @@ -629,7 +629,7 @@
    2.72  %
    2.73  \isatagquoteme
    2.74  \isacommand{lemma}\isamarkupfalse%
    2.75 -\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
    2.76 +\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
    2.77  \ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
    2.78  \ \ \isacommand{by}\isamarkupfalse%
    2.79  \ simp\isanewline
    2.80 @@ -637,7 +637,7 @@
    2.81  \isacommand{declare}\isamarkupfalse%
    2.82  \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
    2.83  \isacommand{declare}\isamarkupfalse%
    2.84 -\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
    2.85 +\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
    2.86  \endisatagquoteme
    2.87  {\isafoldquoteme}%
    2.88  %
    2.89 @@ -715,13 +715,13 @@
    2.90  \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
    2.91  \ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
    2.92  \isacommand{declare}\isamarkupfalse%
    2.93 -\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
    2.94 +\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ del{\isacharbrackright}\isanewline
    2.95  \isacommand{declare}\isamarkupfalse%
    2.96  \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
    2.97  \isacommand{declare}\isamarkupfalse%
    2.98 -\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
    2.99 +\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code{\isacharbrackright}\ \isanewline
   2.100  \isacommand{lemma}\isamarkupfalse%
   2.101 -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   2.102 +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   2.103  \ simp%
   2.104  \endisataginvisible
   2.105  {\isafoldinvisible}%
   2.106 @@ -784,15 +784,15 @@
   2.107  \newline%
   2.108  \verb|fun eqop A_ a b = eq A_ a b;|\newline%
   2.109  \newline%
   2.110 -\verb|fun member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys|\newline%
   2.111 -\verb|  |\verb,|,\verb| member A_ x [] = false;|\newline%
   2.112 +\verb|fun member A_ x [] = false|\newline%
   2.113 +\verb|  |\verb,|,\verb| member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;|\newline%
   2.114  \newline%
   2.115 -\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
   2.116 -\verb|  (if member A_ z xs|\newline%
   2.117 -\verb|    then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
   2.118 -\verb|           else collect_duplicates A_ xs (z :: ys) zs)|\newline%
   2.119 -\verb|    else collect_duplicates A_ (z :: xs) (z :: ys) zs)|\newline%
   2.120 -\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys [] = xs;|\newline%
   2.121 +\verb|fun collect_duplicates A_ xs ys [] = xs|\newline%
   2.122 +\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys (z :: zs) =|\newline%
   2.123 +\verb|    (if member A_ z xs|\newline%
   2.124 +\verb|      then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
   2.125 +\verb|             else collect_duplicates A_ xs (z :: ys) zs)|\newline%
   2.126 +\verb|      else collect_duplicates A_ (z :: xs) (z :: ys) zs);|\newline%
   2.127  \newline%
   2.128  \verb|end; (*struct Example*)|%
   2.129  \end{isamarkuptext}%
   2.130 @@ -835,11 +835,11 @@
   2.131  \isakeyword{begin}\isanewline
   2.132  \isanewline
   2.133  \isacommand{definition}\isamarkupfalse%
   2.134 -\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
   2.135 +\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
   2.136  \ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
   2.137  \isanewline
   2.138  \isacommand{definition}\isamarkupfalse%
   2.139 -\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
   2.140 +\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
   2.141  \ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
   2.142  \isanewline
   2.143  \isacommand{instance}\isamarkupfalse%
   2.144 @@ -852,7 +852,7 @@
   2.145  \isanewline
   2.146  \isanewline
   2.147  \isacommand{lemma}\isamarkupfalse%
   2.148 -\ order{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.149 +\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   2.150  \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   2.151  \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
   2.152  \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   2.153 @@ -884,7 +884,7 @@
   2.154  %
   2.155  \isatagquoteme
   2.156  \isacommand{lemma}\isamarkupfalse%
   2.157 -\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.158 +\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   2.159  \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   2.160  \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
   2.161  \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   2.162 @@ -1007,7 +1007,7 @@
   2.163  %
   2.164  \isatagquoteme
   2.165  \isacommand{lemma}\isamarkupfalse%
   2.166 -\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   2.167 +\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
   2.168  \ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
   2.169  \ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
   2.170  \ \ \isacommand{by}\isamarkupfalse%
   2.171 @@ -1038,8 +1038,8 @@
   2.172  \newline%
   2.173  \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
   2.174  \newline%
   2.175 -\verb|fun null (x :: xs) = false|\newline%
   2.176 -\verb|  |\verb,|,\verb| null [] = true;|\newline%
   2.177 +\verb|fun null [] = true|\newline%
   2.178 +\verb|  |\verb,|,\verb| null (x :: xs) = false;|\newline%
   2.179  \newline%
   2.180  \verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
   2.181  \verb|  |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
     3.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 10 06:45:50 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 10 06:45:53 2008 +0200
     3.3 @@ -993,7 +993,7 @@
     3.4      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     3.5      ;
     3.6  
     3.7 -    'code' ('func' | 'inline') ( 'del' )?
     3.8 +    'code' ( 'inline' ) ? ( 'del' ) ?
     3.9      ;
    3.10    \end{rail}
    3.11  
    3.12 @@ -1080,13 +1080,13 @@
    3.13    are not required to have a definition by means of defining equations;
    3.14    if needed these are implemented by program abort instead.
    3.15  
    3.16 -  \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
    3.17 -  with option ``@{text "del:"}'' deselects) a defining equation for
    3.18 +  \item [@{attribute (HOL) code}] explicitly selects (or
    3.19 +  with option ``@{text "del"}'' deselects) a defining equation for
    3.20    code generation.  Usually packages introducing defining equations
    3.21    provide a reasonable default setup for selection.
    3.22  
    3.23    \item [@{attribute (HOL) code}@{text inline}] declares (or with
    3.24 -  option ``@{text "del:"}'' removes) inlining theorems which are
    3.25 +  option ``@{text "del"}'' removes) inlining theorems which are
    3.26    applied as rewrite rules to any defining equation during
    3.27    preprocessing.
    3.28  
     4.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 10 06:45:50 2008 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 10 06:45:53 2008 +0200
     4.3 @@ -997,7 +997,7 @@
     4.4      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     4.5      ;
     4.6  
     4.7 -    'code' ('func' | 'inline') ( 'del' )?
     4.8 +    'code' ( 'inline' ) ? ( 'del' ) ?
     4.9      ;
    4.10    \end{rail}
    4.11  
    4.12 @@ -1081,13 +1081,13 @@
    4.13    are not required to have a definition by means of defining equations;
    4.14    if needed these are implemented by program abort instead.
    4.15  
    4.16 -  \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
    4.17 -  with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
    4.18 +  \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or
    4.19 +  with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for
    4.20    code generation.  Usually packages introducing defining equations
    4.21    provide a reasonable default setup for selection.
    4.22  
    4.23    \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
    4.24 -  option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are
    4.25 +  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
    4.26    applied as rewrite rules to any defining equation during
    4.27    preprocessing.
    4.28  
     5.1 --- a/src/HOL/Code_Eval.thy	Fri Oct 10 06:45:50 2008 +0200
     5.2 +++ b/src/HOL/Code_Eval.thy	Fri Oct 10 06:45:53 2008 +0200
     5.3 @@ -133,14 +133,14 @@
     5.4  
     5.5  subsubsection {* Code generator setup *}
     5.6  
     5.7 -lemmas [code func del] = term.recs term.cases term.size
     5.8 -lemma [code func, code func del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
     5.9 +lemmas [code del] = term.recs term.cases term.size
    5.10 +lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
    5.11  
    5.12 -lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
    5.13 -lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
    5.14 -lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
    5.15 +lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
    5.16 +lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
    5.17 +lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
    5.18  
    5.19 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code func]: "Code_Eval.term_of c =
    5.20 +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
    5.21      (let (n, m) = nibble_pair_of_char c
    5.22    in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    5.23      (Code_Eval.term_of n)) (Code_Eval.term_of m))"
     6.1 --- a/src/HOL/Code_Setup.thy	Fri Oct 10 06:45:50 2008 +0200
     6.2 +++ b/src/HOL/Code_Setup.thy	Fri Oct 10 06:45:53 2008 +0200
     6.3 @@ -21,32 +21,32 @@
     6.4  
     6.5  text {* Code equations *}
     6.6  
     6.7 -lemma [code func]:
     6.8 +lemma [code]:
     6.9    shows "False \<and> x \<longleftrightarrow> False"
    6.10      and "True \<and> x \<longleftrightarrow> x"
    6.11      and "x \<and> False \<longleftrightarrow> False"
    6.12      and "x \<and> True \<longleftrightarrow> x" by simp_all
    6.13  
    6.14 -lemma [code func]:
    6.15 +lemma [code]:
    6.16    shows "False \<or> x \<longleftrightarrow> x"
    6.17      and "True \<or> x \<longleftrightarrow> True"
    6.18      and "x \<or> False \<longleftrightarrow> x"
    6.19      and "x \<or> True \<longleftrightarrow> True" by simp_all
    6.20  
    6.21 -lemma [code func]:
    6.22 +lemma [code]:
    6.23    shows "\<not> True \<longleftrightarrow> False"
    6.24      and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
    6.25  
    6.26 -lemmas [code func] = Let_def if_True if_False
    6.27 +lemmas [code] = Let_def if_True if_False
    6.28  
    6.29 -lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
    6.30 +lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
    6.31  
    6.32  text {* Equality *}
    6.33  
    6.34  context eq
    6.35  begin
    6.36  
    6.37 -lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
    6.38 +lemma equals_eq [code inline, code]: "op = \<equiv> eq"
    6.39    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    6.40  
    6.41  declare eq [code unfold, code inline del]
     7.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Oct 10 06:45:50 2008 +0200
     7.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Oct 10 06:45:53 2008 +0200
     7.3 @@ -481,7 +481,7 @@
     7.4    "numgcdh (C i) = (\<lambda>g. zgcd i g)"
     7.5    "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
     7.6    "numgcdh t = (\<lambda>g. 1)"
     7.7 -defs numgcd_def [code func]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
     7.8 +defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
     7.9  
    7.10  recdef reducecoeffh "measure size"
    7.11    "reducecoeffh (C i) = (\<lambda> g. C (i div g))"
     8.1 --- a/src/HOL/Datatype.thy	Fri Oct 10 06:45:50 2008 +0200
     8.2 +++ b/src/HOL/Datatype.thy	Fri Oct 10 06:45:53 2008 +0200
     8.3 @@ -635,7 +635,7 @@
     8.4  definition
     8.5    option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
     8.6  where
     8.7 -  [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
     8.8 +  [code del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
     8.9  
    8.10  lemma option_map_None [simp, code]: "option_map f None = None"
    8.11    by (simp add: option_map_def)
     9.1 --- a/src/HOL/Divides.thy	Fri Oct 10 06:45:50 2008 +0200
     9.2 +++ b/src/HOL/Divides.thy	Fri Oct 10 06:45:53 2008 +0200
     9.3 @@ -127,7 +127,7 @@
     9.4    note that ultimately show thesis by blast
     9.5  qed
     9.6  
     9.7 -lemma dvd_eq_mod_eq_0 [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
     9.8 +lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
     9.9  proof
    9.10    assume "b mod a = 0"
    9.11    with mod_div_equality [of b a] have "b div a * a = b" by simp
    9.12 @@ -230,7 +230,7 @@
    9.13  begin
    9.14  
    9.15  definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
    9.16 -  [code func del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
    9.17 +  [code del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
    9.18  
    9.19  definition div_nat where
    9.20    "m div n = fst (divmod m n)"
    10.1 --- a/src/HOL/Equiv_Relations.thy	Fri Oct 10 06:45:50 2008 +0200
    10.2 +++ b/src/HOL/Equiv_Relations.thy	Fri Oct 10 06:45:53 2008 +0200
    10.3 @@ -94,7 +94,7 @@
    10.4  subsection {* Quotients *}
    10.5  
    10.6  definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"  (infixl "'/'/" 90) where
    10.7 -  [code func del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
    10.8 +  [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
    10.9  
   10.10  lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
   10.11    by (unfold quotient_def) blast
    11.1 --- a/src/HOL/Fun.thy	Fri Oct 10 06:45:50 2008 +0200
    11.2 +++ b/src/HOL/Fun.thy	Fri Oct 10 06:45:53 2008 +0200
    11.3 @@ -117,7 +117,7 @@
    11.4  
    11.5  definition
    11.6    bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
    11.7 -  [code func del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
    11.8 +  [code del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
    11.9  
   11.10  constdefs
   11.11    surj :: "('a => 'b) => bool"                   (*surjective*)
    12.1 --- a/src/HOL/HOL.thy	Fri Oct 10 06:45:50 2008 +0200
    12.2 +++ b/src/HOL/HOL.thy	Fri Oct 10 06:45:53 2008 +0200
    12.3 @@ -1227,7 +1227,7 @@
    12.4  
    12.5  constdefs
    12.6    simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
    12.7 -  [code func del]: "simp_implies \<equiv> op ==>"
    12.8 +  [code del]: "simp_implies \<equiv> op ==>"
    12.9  
   12.10  lemma simp_impliesI:
   12.11    assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
    13.1 --- a/src/HOL/Hyperreal/Integration.thy	Fri Oct 10 06:45:50 2008 +0200
    13.2 +++ b/src/HOL/Hyperreal/Integration.thy	Fri Oct 10 06:45:53 2008 +0200
    13.3 @@ -16,29 +16,29 @@
    13.4    --{*Partitions and tagged partitions etc.*}
    13.5  
    13.6    partition :: "[(real*real),nat => real] => bool" where
    13.7 -  [code func del]: "partition = (%(a,b) D. D 0 = a &
    13.8 +  [code del]: "partition = (%(a,b) D. D 0 = a &
    13.9                           (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
   13.10                                (\<forall>n \<ge> N. D(n) = b)))"
   13.11  
   13.12  definition
   13.13    psize :: "(nat => real) => nat" where
   13.14 -  [code func del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
   13.15 +  [code del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
   13.16                        (\<forall>n \<ge> N. D(n) = D(N)))"
   13.17  
   13.18  definition
   13.19    tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
   13.20 -  [code func del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
   13.21 +  [code del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
   13.22                            (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
   13.23  
   13.24    --{*Gauges and gauge-fine divisions*}
   13.25  
   13.26  definition
   13.27    gauge :: "[real => bool, real => real] => bool" where
   13.28 -  [code func del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
   13.29 +  [code del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
   13.30  
   13.31  definition
   13.32    fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
   13.33 -  [code func del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
   13.34 +  [code del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
   13.35  
   13.36    --{*Riemann sum*}
   13.37  
   13.38 @@ -50,7 +50,7 @@
   13.39  
   13.40  definition
   13.41    Integral :: "[(real*real),real=>real,real] => bool" where
   13.42 -  [code func del]: "Integral = (%(a,b) f k. \<forall>e > 0.
   13.43 +  [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
   13.44                                 (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
   13.45                                 (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
   13.46                                           \<bar>rsum(D,p) f - k\<bar> < e)))"
    14.1 --- a/src/HOL/Hyperreal/Lim.thy	Fri Oct 10 06:45:50 2008 +0200
    14.2 +++ b/src/HOL/Hyperreal/Lim.thy	Fri Oct 10 06:45:53 2008 +0200
    14.3 @@ -16,7 +16,7 @@
    14.4  definition
    14.5    LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
    14.6          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
    14.7 -  [code func del]: "f -- a --> L =
    14.8 +  [code del]: "f -- a --> L =
    14.9       (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
   14.10          --> norm (f x - L) < r)"
   14.11  
   14.12 @@ -26,7 +26,7 @@
   14.13  
   14.14  definition
   14.15    isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
   14.16 -  [code func del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
   14.17 +  [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
   14.18  
   14.19  
   14.20  subsection {* Limits of Functions *}
    15.1 --- a/src/HOL/Hyperreal/SEQ.thy	Fri Oct 10 06:45:50 2008 +0200
    15.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Fri Oct 10 06:45:53 2008 +0200
    15.3 @@ -15,13 +15,13 @@
    15.4  definition
    15.5    Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
    15.6      --{*Standard definition of sequence converging to zero*}
    15.7 -  [code func del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
    15.8 +  [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
    15.9  
   15.10  definition
   15.11    LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
   15.12      ("((_)/ ----> (_))" [60, 60] 60) where
   15.13      --{*Standard definition of convergence of sequence*}
   15.14 -  [code func del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
   15.15 +  [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
   15.16  
   15.17  definition
   15.18    lim :: "(nat => 'a::real_normed_vector) => 'a" where
   15.19 @@ -36,22 +36,22 @@
   15.20  definition
   15.21    Bseq :: "(nat => 'a::real_normed_vector) => bool" where
   15.22      --{*Standard definition for bounded sequence*}
   15.23 -  [code func del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
   15.24 +  [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
   15.25  
   15.26  definition
   15.27    monoseq :: "(nat=>real)=>bool" where
   15.28      --{*Definition for monotonicity*}
   15.29 -  [code func del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
   15.30 +  [code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
   15.31  
   15.32  definition
   15.33    subseq :: "(nat => nat) => bool" where
   15.34      --{*Definition of subsequence*}
   15.35 -  [code func del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
   15.36 +  [code del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
   15.37  
   15.38  definition
   15.39    Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
   15.40      --{*Standard definition of the Cauchy condition*}
   15.41 -  [code func del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
   15.42 +  [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
   15.43  
   15.44  
   15.45  subsection {* Bounded Sequences *}
    16.1 --- a/src/HOL/Int.thy	Fri Oct 10 06:45:50 2008 +0200
    16.2 +++ b/src/HOL/Int.thy	Fri Oct 10 06:45:53 2008 +0200
    16.3 @@ -24,7 +24,7 @@
    16.4  definition
    16.5    intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
    16.6  where
    16.7 -  [code func del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
    16.8 +  [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
    16.9  
   16.10  typedef (Integ)
   16.11    int = "UNIV//intrel"
   16.12 @@ -34,34 +34,34 @@
   16.13  begin
   16.14  
   16.15  definition
   16.16 -  Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
   16.17 +  Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
   16.18  
   16.19  definition
   16.20 -  One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
   16.21 +  One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
   16.22  
   16.23  definition
   16.24 -  add_int_def [code func del]: "z + w = Abs_Integ
   16.25 +  add_int_def [code del]: "z + w = Abs_Integ
   16.26      (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
   16.27        intrel `` {(x + u, y + v)})"
   16.28  
   16.29  definition
   16.30 -  minus_int_def [code func del]:
   16.31 +  minus_int_def [code del]:
   16.32      "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
   16.33  
   16.34  definition
   16.35 -  diff_int_def [code func del]:  "z - w = z + (-w \<Colon> int)"
   16.36 +  diff_int_def [code del]:  "z - w = z + (-w \<Colon> int)"
   16.37  
   16.38  definition
   16.39 -  mult_int_def [code func del]: "z * w = Abs_Integ
   16.40 +  mult_int_def [code del]: "z * w = Abs_Integ
   16.41      (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
   16.42        intrel `` {(x*u + y*v, x*v + y*u)})"
   16.43  
   16.44  definition
   16.45 -  le_int_def [code func del]:
   16.46 +  le_int_def [code del]:
   16.47     "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
   16.48  
   16.49  definition
   16.50 -  less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
   16.51 +  less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
   16.52  
   16.53  definition
   16.54    zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
   16.55 @@ -298,7 +298,7 @@
   16.56  definition
   16.57    of_int :: "int \<Rightarrow> 'a"
   16.58  where
   16.59 -  [code func del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
   16.60 +  [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
   16.61  
   16.62  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
   16.63  proof -
   16.64 @@ -390,7 +390,7 @@
   16.65  definition
   16.66    nat :: "int \<Rightarrow> nat"
   16.67  where
   16.68 -  [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   16.69 +  [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   16.70  
   16.71  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
   16.72  proof -
   16.73 @@ -585,19 +585,19 @@
   16.74  
   16.75  definition
   16.76    Pls :: int where
   16.77 -  [code func del]: "Pls = 0"
   16.78 +  [code del]: "Pls = 0"
   16.79  
   16.80  definition
   16.81    Min :: int where
   16.82 -  [code func del]: "Min = - 1"
   16.83 +  [code del]: "Min = - 1"
   16.84  
   16.85  definition
   16.86    Bit0 :: "int \<Rightarrow> int" where
   16.87 -  [code func del]: "Bit0 k = k + k"
   16.88 +  [code del]: "Bit0 k = k + k"
   16.89  
   16.90  definition
   16.91    Bit1 :: "int \<Rightarrow> int" where
   16.92 -  [code func del]: "Bit1 k = 1 + k + k"
   16.93 +  [code del]: "Bit1 k = 1 + k + k"
   16.94  
   16.95  class number = type + -- {* for numeric types: nat, int, real, \dots *}
   16.96    fixes number_of :: "int \<Rightarrow> 'a"
   16.97 @@ -622,11 +622,11 @@
   16.98  
   16.99  definition
  16.100    succ :: "int \<Rightarrow> int" where
  16.101 -  [code func del]: "succ k = k + 1"
  16.102 +  [code del]: "succ k = k + 1"
  16.103  
  16.104  definition
  16.105    pred :: "int \<Rightarrow> int" where
  16.106 -  [code func del]: "pred k = k - 1"
  16.107 +  [code del]: "pred k = k - 1"
  16.108  
  16.109  lemmas
  16.110    max_number_of [simp] = max_def
  16.111 @@ -785,7 +785,7 @@
  16.112  begin
  16.113  
  16.114  definition
  16.115 -  int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
  16.116 +  int_number_of_def [code del]: "number_of w = (of_int w \<Colon> int)"
  16.117  
  16.118  instance
  16.119    by intro_classes (simp only: int_number_of_def)
  16.120 @@ -1167,7 +1167,7 @@
  16.121  definition
  16.122    Ints  :: "'a set"
  16.123  where
  16.124 -  [code func del]: "Ints = range of_int"
  16.125 +  [code del]: "Ints = range of_int"
  16.126  
  16.127  end
  16.128  
  16.129 @@ -1799,36 +1799,36 @@
  16.130  
  16.131  code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
  16.132  
  16.133 -lemmas pred_succ_numeral_code [code func] =
  16.134 +lemmas pred_succ_numeral_code [code] =
  16.135    pred_bin_simps succ_bin_simps
  16.136  
  16.137 -lemmas plus_numeral_code [code func] =
  16.138 +lemmas plus_numeral_code [code] =
  16.139    add_bin_simps
  16.140    arith_extra_simps(1) [where 'a = int]
  16.141  
  16.142 -lemmas minus_numeral_code [code func] =
  16.143 +lemmas minus_numeral_code [code] =
  16.144    minus_bin_simps
  16.145    arith_extra_simps(2) [where 'a = int]
  16.146    arith_extra_simps(5) [where 'a = int]
  16.147  
  16.148 -lemmas times_numeral_code [code func] =
  16.149 +lemmas times_numeral_code [code] =
  16.150    mult_bin_simps
  16.151    arith_extra_simps(4) [where 'a = int]
  16.152  
  16.153  instantiation int :: eq
  16.154  begin
  16.155  
  16.156 -definition [code func del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
  16.157 +definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
  16.158  
  16.159  instance by default (simp add: eq_int_def)
  16.160  
  16.161  end
  16.162  
  16.163 -lemma eq_number_of_int_code [code func]:
  16.164 +lemma eq_number_of_int_code [code]:
  16.165    "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
  16.166    unfolding eq_int_def number_of_is_id ..
  16.167  
  16.168 -lemma eq_int_code [code func]:
  16.169 +lemma eq_int_code [code]:
  16.170    "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
  16.171    "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
  16.172    "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
  16.173 @@ -1859,11 +1859,11 @@
  16.174    "eq_class.eq (k::int) k \<longleftrightarrow> True"
  16.175    by (rule HOL.eq_refl)
  16.176  
  16.177 -lemma less_eq_number_of_int_code [code func]:
  16.178 +lemma less_eq_number_of_int_code [code]:
  16.179    "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
  16.180    unfolding number_of_is_id ..
  16.181  
  16.182 -lemma less_eq_int_code [code func]:
  16.183 +lemma less_eq_int_code [code]:
  16.184    "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
  16.185    "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
  16.186    "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
  16.187 @@ -1890,11 +1890,11 @@
  16.188      (auto simp add: neg_def linorder_not_less group_simps
  16.189        zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def)
  16.190  
  16.191 -lemma less_number_of_int_code [code func]:
  16.192 +lemma less_number_of_int_code [code]:
  16.193    "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
  16.194    unfolding number_of_is_id ..
  16.195  
  16.196 -lemma less_int_code [code func]:
  16.197 +lemma less_int_code [code]:
  16.198    "Int.Pls < Int.Pls \<longleftrightarrow> False"
  16.199    "Int.Pls < Int.Min \<longleftrightarrow> False"
  16.200    "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
  16.201 @@ -1935,11 +1935,11 @@
  16.202  
  16.203  hide (open) const nat_aux
  16.204  
  16.205 -lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
  16.206 +lemma zero_is_num_zero [code, code inline, symmetric, code post]:
  16.207    "(0\<Colon>int) = Numeral0" 
  16.208    by simp
  16.209  
  16.210 -lemma one_is_num_one [code func, code inline, symmetric, code post]:
  16.211 +lemma one_is_num_one [code, code inline, symmetric, code post]:
  16.212    "(1\<Colon>int) = Numeral1" 
  16.213    by simp
  16.214  
    17.1 --- a/src/HOL/IntDiv.thy	Fri Oct 10 06:45:50 2008 +0200
    17.2 +++ b/src/HOL/IntDiv.thy	Fri Oct 10 06:45:53 2008 +0200
    17.3 @@ -14,13 +14,13 @@
    17.4  constdefs
    17.5    quorem :: "(int*int) * (int*int) => bool"
    17.6      --{*definition of quotient and remainder*}
    17.7 -    [code func]: "quorem == %((a,b), (q,r)).
    17.8 +    [code]: "quorem == %((a,b), (q,r)).
    17.9                        a = b*q + r &
   17.10                        (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
   17.11  
   17.12    adjust :: "[int, int*int] => int*int"
   17.13      --{*for the division algorithm*}
   17.14 -    [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
   17.15 +    [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
   17.16                           else (2*q, r)"
   17.17  
   17.18  text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
   17.19 @@ -46,7 +46,7 @@
   17.20  text{*algorithm for the general case @{term "b\<noteq>0"}*}
   17.21  constdefs
   17.22    negateSnd :: "int*int => int*int"
   17.23 -    [code func]: "negateSnd == %(q,r). (q,-r)"
   17.24 +    [code]: "negateSnd == %(q,r). (q,-r)"
   17.25  
   17.26  definition
   17.27    divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
   17.28 @@ -1477,7 +1477,7 @@
   17.29  context ring_1
   17.30  begin
   17.31  
   17.32 -lemma of_int_num [code func]:
   17.33 +lemma of_int_num [code]:
   17.34    "of_int k = (if k = 0 then 0 else if k < 0 then
   17.35       - of_int (- k) else let
   17.36         (l, m) = divAlg (k, 2);
    18.1 --- a/src/HOL/Lattices.thy	Fri Oct 10 06:45:50 2008 +0200
    18.2 +++ b/src/HOL/Lattices.thy	Fri Oct 10 06:45:53 2008 +0200
    18.3 @@ -9,7 +9,7 @@
    18.4  imports Fun
    18.5  begin
    18.6  
    18.7 -subsection{* Lattices *}
    18.8 +subsection {* Lattices *}
    18.9  
   18.10  notation
   18.11    less_eq  (infix "\<sqsubseteq>" 50) and
   18.12 @@ -40,7 +40,7 @@
   18.13  class lattice = lower_semilattice + upper_semilattice
   18.14  
   18.15  
   18.16 -subsubsection{* Intro and elim rules*}
   18.17 +subsubsection {* Intro and elim rules*}
   18.18  
   18.19  context lower_semilattice
   18.20  begin
   18.21 @@ -512,10 +512,10 @@
   18.22  begin
   18.23  
   18.24  definition
   18.25 -  inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   18.26 +  inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   18.27  
   18.28  definition
   18.29 -  sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   18.30 +  sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   18.31  
   18.32  instance
   18.33  apply intro_classes
   18.34 @@ -536,10 +536,10 @@
   18.35  begin
   18.36  
   18.37  definition
   18.38 -  Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   18.39 +  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   18.40  
   18.41  definition
   18.42 -  Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   18.43 +  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   18.44  
   18.45  instance
   18.46    by intro_classes
    19.1 --- a/src/HOL/Library/Array.thy	Fri Oct 10 06:45:50 2008 +0200
    19.2 +++ b/src/HOL/Library/Array.thy	Fri Oct 10 06:45:53 2008 +0200
    19.3 @@ -107,14 +107,14 @@
    19.4  
    19.5  subsection {* Properties *}
    19.6  
    19.7 -lemma array_make [code func]:
    19.8 +lemma array_make [code]:
    19.9    "Array.new n x = make n (\<lambda>_. x)"
   19.10    by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
   19.11      monad_simp array_of_list_replicate [symmetric]
   19.12      map_replicate_trivial replicate_append_same
   19.13      of_list_def)
   19.14  
   19.15 -lemma array_of_list_make [code func]:
   19.16 +lemma array_of_list_make [code]:
   19.17    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   19.18    unfolding make_def map_nth ..
   19.19  
   19.20 @@ -126,28 +126,28 @@
   19.21  definition new' where
   19.22    [code del]: "new' = Array.new o nat_of_index"
   19.23  hide (open) const new'
   19.24 -lemma [code func]:
   19.25 +lemma [code]:
   19.26    "Array.new = Array.new' o index_of_nat"
   19.27    by (simp add: new'_def o_def)
   19.28  
   19.29  definition of_list' where
   19.30    [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
   19.31  hide (open) const of_list'
   19.32 -lemma [code func]:
   19.33 +lemma [code]:
   19.34    "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
   19.35    by (simp add: of_list'_def)
   19.36  
   19.37  definition make' where
   19.38    [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
   19.39  hide (open) const make'
   19.40 -lemma [code func]:
   19.41 +lemma [code]:
   19.42    "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
   19.43    by (simp add: make'_def o_def)
   19.44  
   19.45  definition length' where
   19.46    [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
   19.47  hide (open) const length'
   19.48 -lemma [code func]:
   19.49 +lemma [code]:
   19.50    "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
   19.51    by (simp add: length'_def monad_simp',
   19.52      simp add: liftM_def comp_def monad_simp,
   19.53 @@ -156,14 +156,14 @@
   19.54  definition nth' where
   19.55    [code del]: "nth' a = Array.nth a o nat_of_index"
   19.56  hide (open) const nth'
   19.57 -lemma [code func]:
   19.58 +lemma [code]:
   19.59    "Array.nth a n = Array.nth' a (index_of_nat n)"
   19.60    by (simp add: nth'_def)
   19.61  
   19.62  definition upd' where
   19.63    [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
   19.64  hide (open) const upd'
   19.65 -lemma [code func]:
   19.66 +lemma [code]:
   19.67    "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
   19.68    by (simp add: upd'_def monad_simp upd_return)
   19.69  
    20.1 --- a/src/HOL/Library/Char_nat.thy	Fri Oct 10 06:45:50 2008 +0200
    20.2 +++ b/src/HOL/Library/Char_nat.thy	Fri Oct 10 06:45:53 2008 +0200
    20.3 @@ -54,7 +54,7 @@
    20.4    "nibble_of_nat (n mod 16) = nibble_of_nat n"
    20.5    unfolding nibble_of_nat_def Let_def by auto
    20.6  
    20.7 -lemmas [code func] = nibble_of_nat_norm [symmetric]
    20.8 +lemmas [code] = nibble_of_nat_norm [symmetric]
    20.9  
   20.10  lemma nibble_of_nat_simps [simp]:
   20.11    "nibble_of_nat  0 = Nibble0"
   20.12 @@ -75,7 +75,7 @@
   20.13    "nibble_of_nat 15 = NibbleF"
   20.14    unfolding nibble_of_nat_def Let_def by auto
   20.15  
   20.16 -lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
   20.17 +lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
   20.18    [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
   20.19  
   20.20  lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
   20.21 @@ -115,7 +115,7 @@
   20.22    nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
   20.23    "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
   20.24  
   20.25 -lemma nibble_of_pair [code func]:
   20.26 +lemma nibble_of_pair [code]:
   20.27    "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
   20.28    unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
   20.29  
    21.1 --- a/src/HOL/Library/Char_ord.thy	Fri Oct 10 06:45:50 2008 +0200
    21.2 +++ b/src/HOL/Library/Char_ord.thy	Fri Oct 10 06:45:53 2008 +0200
    21.3 @@ -64,11 +64,11 @@
    21.4  begin
    21.5  
    21.6  definition
    21.7 -  char_less_eq_def [code func del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    21.8 +  char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    21.9      n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
   21.10  
   21.11  definition
   21.12 -  char_less_def [code func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
   21.13 +  char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
   21.14      n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
   21.15  
   21.16  instance
   21.17 @@ -90,7 +90,7 @@
   21.18  
   21.19  end
   21.20  
   21.21 -lemma [simp, code func]:
   21.22 +lemma [simp, code]:
   21.23    shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
   21.24    and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
   21.25    unfolding char_less_eq_def char_less_def by simp_all
    22.1 --- a/src/HOL/Library/Code_Char_chr.thy	Fri Oct 10 06:45:50 2008 +0200
    22.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Fri Oct 10 06:45:53 2008 +0200
    22.3 @@ -12,28 +12,28 @@
    22.4  definition
    22.5    "int_of_char = int o nat_of_char"
    22.6  
    22.7 -lemma [code func]:
    22.8 +lemma [code]:
    22.9    "nat_of_char = nat o int_of_char"
   22.10    unfolding int_of_char_def by (simp add: expand_fun_eq)
   22.11  
   22.12  definition
   22.13    "char_of_int = char_of_nat o nat"
   22.14  
   22.15 -lemma [code func]:
   22.16 +lemma [code]:
   22.17    "char_of_nat = char_of_int o int"
   22.18    unfolding char_of_int_def by (simp add: expand_fun_eq)
   22.19  
   22.20 -lemmas [code func del] = char.recs char.cases char.size
   22.21 +lemmas [code del] = char.recs char.cases char.size
   22.22  
   22.23 -lemma [code func, code inline]:
   22.24 +lemma [code, code inline]:
   22.25    "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
   22.26    by (cases c) (auto simp add: nibble_pair_of_nat_char)
   22.27  
   22.28 -lemma [code func, code inline]:
   22.29 +lemma [code, code inline]:
   22.30    "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
   22.31    by (cases c) (auto simp add: nibble_pair_of_nat_char)
   22.32  
   22.33 -lemma [code func]:
   22.34 +lemma [code]:
   22.35    "size (c\<Colon>char) = 0"
   22.36    by (cases c) auto
   22.37  
    23.1 --- a/src/HOL/Library/Code_Index.thy	Fri Oct 10 06:45:50 2008 +0200
    23.2 +++ b/src/HOL/Library/Code_Index.thy	Fri Oct 10 06:45:53 2008 +0200
    23.3 @@ -64,7 +64,7 @@
    23.4  instantiation index :: zero
    23.5  begin
    23.6  
    23.7 -definition [simp, code func del]:
    23.8 +definition [simp, code del]:
    23.9    "0 = index_of_nat 0"
   23.10  
   23.11  instance ..
   23.12 @@ -87,12 +87,12 @@
   23.13    then show "P k" by simp
   23.14  qed simp_all
   23.15  
   23.16 -lemmas [code func del] = index.recs index.cases
   23.17 +lemmas [code del] = index.recs index.cases
   23.18  
   23.19  declare index_case [case_names nat, cases type: index]
   23.20  declare index.induct [case_names nat, induct type: index]
   23.21  
   23.22 -lemma [code func]:
   23.23 +lemma [code]:
   23.24    "index_size = nat_of_index"
   23.25  proof (rule ext)
   23.26    fix k
   23.27 @@ -102,7 +102,7 @@
   23.28    finally show "index_size k = nat_of_index k" .
   23.29  qed
   23.30  
   23.31 -lemma [code func]:
   23.32 +lemma [code]:
   23.33    "size = nat_of_index"
   23.34  proof (rule ext)
   23.35    fix k
   23.36 @@ -110,7 +110,7 @@
   23.37    by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
   23.38  qed
   23.39  
   23.40 -lemma [code func]:
   23.41 +lemma [code]:
   23.42    "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
   23.43    by (cases k, cases l) (simp add: eq)
   23.44  
   23.45 @@ -143,63 +143,63 @@
   23.46  instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
   23.47  begin
   23.48  
   23.49 -lemma zero_index_code [code inline, code func]:
   23.50 +lemma zero_index_code [code inline, code]:
   23.51    "(0\<Colon>index) = Numeral0"
   23.52    by (simp add: number_of_index_def Pls_def)
   23.53  lemma [code post]: "Numeral0 = (0\<Colon>index)"
   23.54    using zero_index_code ..
   23.55  
   23.56 -definition [simp, code func del]:
   23.57 +definition [simp, code del]:
   23.58    "(1\<Colon>index) = index_of_nat 1"
   23.59  
   23.60 -lemma one_index_code [code inline, code func]:
   23.61 +lemma one_index_code [code inline, code]:
   23.62    "(1\<Colon>index) = Numeral1"
   23.63    by (simp add: number_of_index_def Pls_def Bit1_def)
   23.64  lemma [code post]: "Numeral1 = (1\<Colon>index)"
   23.65    using one_index_code ..
   23.66  
   23.67 -definition [simp, code func del]:
   23.68 +definition [simp, code del]:
   23.69    "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
   23.70  
   23.71 -lemma plus_index_code [code func]:
   23.72 +lemma plus_index_code [code]:
   23.73    "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
   23.74    by simp
   23.75  
   23.76 -definition [simp, code func del]:
   23.77 +definition [simp, code del]:
   23.78    "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
   23.79  
   23.80 -definition [simp, code func del]:
   23.81 +definition [simp, code del]:
   23.82    "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
   23.83  
   23.84 -lemma times_index_code [code func]:
   23.85 +lemma times_index_code [code]:
   23.86    "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
   23.87    by simp
   23.88  
   23.89 -definition [simp, code func del]:
   23.90 +definition [simp, code del]:
   23.91    "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
   23.92  
   23.93 -definition [simp, code func del]:
   23.94 +definition [simp, code del]:
   23.95    "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
   23.96  
   23.97 -lemma div_index_code [code func]:
   23.98 +lemma div_index_code [code]:
   23.99    "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
  23.100    by simp
  23.101  
  23.102 -lemma mod_index_code [code func]:
  23.103 +lemma mod_index_code [code]:
  23.104    "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
  23.105    by simp
  23.106  
  23.107 -definition [simp, code func del]:
  23.108 +definition [simp, code del]:
  23.109    "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
  23.110  
  23.111 -definition [simp, code func del]:
  23.112 +definition [simp, code del]:
  23.113    "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
  23.114  
  23.115 -lemma less_eq_index_code [code func]:
  23.116 +lemma less_eq_index_code [code]:
  23.117    "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
  23.118    by simp
  23.119  
  23.120 -lemma less_index_code [code func]:
  23.121 +lemma less_index_code [code]:
  23.122    "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
  23.123    by simp
  23.124  
  23.125 @@ -260,25 +260,25 @@
  23.126  definition
  23.127    minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
  23.128  where
  23.129 -  [code func del]: "minus_index_aux = op -"
  23.130 +  [code del]: "minus_index_aux = op -"
  23.131  
  23.132 -lemma [code func]: "op - = minus_index_aux"
  23.133 +lemma [code]: "op - = minus_index_aux"
  23.134    using minus_index_aux_def ..
  23.135  
  23.136  definition
  23.137    div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index"
  23.138  where
  23.139 -  [code func del]: "div_mod_index n m = (n div m, n mod m)"
  23.140 +  [code del]: "div_mod_index n m = (n div m, n mod m)"
  23.141  
  23.142 -lemma [code func]:
  23.143 +lemma [code]:
  23.144    "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
  23.145    unfolding div_mod_index_def by auto
  23.146  
  23.147 -lemma [code func]:
  23.148 +lemma [code]:
  23.149    "n div m = fst (div_mod_index n m)"
  23.150    unfolding div_mod_index_def by simp
  23.151  
  23.152 -lemma [code func]:
  23.153 +lemma [code]:
  23.154    "n mod m = snd (div_mod_index n m)"
  23.155    unfolding div_mod_index_def by simp
  23.156  
  23.157 @@ -340,7 +340,7 @@
  23.158  
  23.159  text {* Evaluation *}
  23.160  
  23.161 -lemma [code func, code func del]:
  23.162 +lemma [code, code del]:
  23.163    "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
  23.164  
  23.165  code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
    24.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Oct 10 06:45:50 2008 +0200
    24.2 +++ b/src/HOL/Library/Code_Integer.thy	Fri Oct 10 06:45:53 2008 +0200
    24.3 @@ -92,7 +92,7 @@
    24.4  
    24.5  text {* Evaluation *}
    24.6  
    24.7 -lemma [code func, code func del]:
    24.8 +lemma [code, code del]:
    24.9    "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" ..
   24.10  
   24.11  code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
    25.1 --- a/src/HOL/Library/Code_Message.thy	Fri Oct 10 06:45:50 2008 +0200
    25.2 +++ b/src/HOL/Library/Code_Message.thy	Fri Oct 10 06:45:53 2008 +0200
    25.3 @@ -12,12 +12,12 @@
    25.4  
    25.5  datatype message_string = STR string
    25.6  
    25.7 -lemmas [code func del] = message_string.recs message_string.cases
    25.8 +lemmas [code del] = message_string.recs message_string.cases
    25.9  
   25.10 -lemma [code func]: "size (s\<Colon>message_string) = 0"
   25.11 +lemma [code]: "size (s\<Colon>message_string) = 0"
   25.12    by (cases s) simp_all
   25.13  
   25.14 -lemma [code func]: "message_string_size (s\<Colon>message_string) = 0"
   25.15 +lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
   25.16    by (cases s) simp_all
   25.17  
   25.18  subsection {* ML interface *}
    26.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 10 06:45:50 2008 +0200
    26.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 10 06:45:53 2008 +0200
    26.3 @@ -232,7 +232,6 @@
    26.4     of NONE => NONE
    26.5      | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
    26.6          then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
    26.7 -          (*FIXME*)
    26.8    end
    26.9  
   26.10  in
   26.11 @@ -344,13 +343,13 @@
   26.12  definition
   26.13    int :: "nat \<Rightarrow> int"
   26.14  where
   26.15 -  [code func del]: "int = of_nat"
   26.16 +  [code del]: "int = of_nat"
   26.17  
   26.18 -lemma int_code' [code func]:
   26.19 +lemma int_code' [code]:
   26.20    "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   26.21    unfolding int_nat_number_of [folded int_def] ..
   26.22  
   26.23 -lemma nat_code' [code func]:
   26.24 +lemma nat_code' [code]:
   26.25    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   26.26    by auto
   26.27  
   26.28 @@ -434,7 +433,7 @@
   26.29  
   26.30  text {* Evaluation *}
   26.31  
   26.32 -lemma [code func, code func del]:
   26.33 +lemma [code, code del]:
   26.34    "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
   26.35  
   26.36  code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
    27.1 --- a/src/HOL/Library/Enum.thy	Fri Oct 10 06:45:50 2008 +0200
    27.2 +++ b/src/HOL/Library/Enum.thy	Fri Oct 10 06:45:53 2008 +0200
    27.3 @@ -13,7 +13,7 @@
    27.4  
    27.5  class enum = itself +
    27.6    fixes enum :: "'a list"
    27.7 -  assumes UNIV_enum [code func]: "UNIV = set enum"
    27.8 +  assumes UNIV_enum [code]: "UNIV = set enum"
    27.9      and enum_distinct: "distinct enum"
   27.10  begin
   27.11  
   27.12 @@ -49,7 +49,7 @@
   27.13  
   27.14  end
   27.15  
   27.16 -lemma order_fun [code func]:
   27.17 +lemma order_fun [code]:
   27.18    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
   27.19    shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
   27.20      and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
   27.21 @@ -58,10 +58,10 @@
   27.22  
   27.23  subsection {* Quantifiers *}
   27.24  
   27.25 -lemma all_code [code func]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
   27.26 +lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
   27.27    by (simp add: list_all_iff enum_all)
   27.28  
   27.29 -lemma exists_code [code func]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
   27.30 +lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
   27.31    by (simp add: list_all_iff enum_all)
   27.32  
   27.33  
   27.34 @@ -157,7 +157,7 @@
   27.35  begin
   27.36  
   27.37  definition
   27.38 -  [code func del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
   27.39 +  [code del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
   27.40  
   27.41  instance proof
   27.42    show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   27.43 @@ -177,7 +177,7 @@
   27.44  
   27.45  end
   27.46  
   27.47 -lemma enum_fun_code [code func]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
   27.48 +lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
   27.49    in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   27.50    by (simp add: enum_fun_def Let_def)
   27.51  
   27.52 @@ -286,9 +286,9 @@
   27.53  begin
   27.54  
   27.55  definition
   27.56 -  [code func del]: "enum = map (split Char) (product enum enum)"
   27.57 +  [code del]: "enum = map (split Char) (product enum enum)"
   27.58  
   27.59 -lemma enum_char [code func]:
   27.60 +lemma enum_char [code]:
   27.61    "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   27.62    Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   27.63    Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
    28.1 --- a/src/HOL/Library/GCD.thy	Fri Oct 10 06:45:50 2008 +0200
    28.2 +++ b/src/HOL/Library/GCD.thy	Fri Oct 10 06:45:53 2008 +0200
    28.3 @@ -18,7 +18,7 @@
    28.4  
    28.5  definition
    28.6    is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
    28.7 -  [code func del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    28.8 +  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    28.9      (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
   28.10  
   28.11  text {* Uniqueness *}
   28.12 @@ -776,7 +776,7 @@
   28.13    thus ?thesis by (simp add: zlcm_def)
   28.14  qed
   28.15  
   28.16 -lemma zgcd_code [code func]:
   28.17 +lemma zgcd_code [code]:
   28.18    "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   28.19    by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
   28.20  
    29.1 --- a/src/HOL/Library/Heap_Monad.thy	Fri Oct 10 06:45:50 2008 +0200
    29.2 +++ b/src/HOL/Library/Heap_Monad.thy	Fri Oct 10 06:45:53 2008 +0200
    29.3 @@ -266,14 +266,14 @@
    29.4  definition
    29.5    Fail :: "message_string \<Rightarrow> exception"
    29.6  where
    29.7 -  [code func del]: "Fail s = Exn"
    29.8 +  [code del]: "Fail s = Exn"
    29.9  
   29.10  definition
   29.11    raise_exc :: "exception \<Rightarrow> 'a Heap"
   29.12  where
   29.13 -  [code func del]: "raise_exc e = raise []"
   29.14 +  [code del]: "raise_exc e = raise []"
   29.15  
   29.16 -lemma raise_raise_exc [code func, code inline]:
   29.17 +lemma raise_raise_exc [code, code inline]:
   29.18    "raise s = raise_exc (Fail (STR s))"
   29.19    unfolding Fail_def raise_exc_def raise_def ..
   29.20  
    30.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Oct 10 06:45:50 2008 +0200
    30.2 +++ b/src/HOL/Library/List_Prefix.thy	Fri Oct 10 06:45:53 2008 +0200
    30.3 @@ -15,10 +15,10 @@
    30.4  begin
    30.5  
    30.6  definition
    30.7 -  prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
    30.8 +  prefix_def [code del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
    30.9  
   30.10  definition
   30.11 -  strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
   30.12 +  strict_prefix_def [code del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
   30.13  
   30.14  instance
   30.15    by intro_classes (auto simp add: prefix_def strict_prefix_def)
   30.16 @@ -374,18 +374,18 @@
   30.17  
   30.18  subsection {* Executable code *}
   30.19  
   30.20 -lemma less_eq_code [code func]:
   30.21 +lemma less_eq_code [code]:
   30.22      "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
   30.23      "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
   30.24      "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   30.25    by simp_all
   30.26  
   30.27 -lemma less_code [code func]:
   30.28 +lemma less_code [code]:
   30.29      "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
   30.30      "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
   30.31      "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
   30.32    unfolding strict_prefix_def by auto
   30.33  
   30.34 -lemmas [code func] = postfix_to_prefix
   30.35 +lemmas [code] = postfix_to_prefix
   30.36  
   30.37  end
    31.1 --- a/src/HOL/Library/List_lexord.thy	Fri Oct 10 06:45:50 2008 +0200
    31.2 +++ b/src/HOL/Library/List_lexord.thy	Fri Oct 10 06:45:53 2008 +0200
    31.3 @@ -13,10 +13,10 @@
    31.4  begin
    31.5  
    31.6  definition
    31.7 -  list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
    31.8 +  list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
    31.9  
   31.10  definition
   31.11 -  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
   31.12 +  list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
   31.13  
   31.14  instance ..
   31.15  
   31.16 @@ -63,10 +63,10 @@
   31.17  begin
   31.18  
   31.19  definition
   31.20 -  [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
   31.21 +  [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
   31.22  
   31.23  definition
   31.24 -  [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
   31.25 +  [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
   31.26  
   31.27  instance
   31.28    by intro_classes
   31.29 @@ -92,13 +92,13 @@
   31.30  lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
   31.31    by (unfold list_le_def) auto
   31.32  
   31.33 -lemma less_code [code func]:
   31.34 +lemma less_code [code]:
   31.35    "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
   31.36    "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
   31.37    "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
   31.38    by simp_all
   31.39  
   31.40 -lemma less_eq_code [code func]:
   31.41 +lemma less_eq_code [code]:
   31.42    "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
   31.43    "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
   31.44    "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
    32.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 10 06:45:50 2008 +0200
    32.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 10 06:45:53 2008 +0200
    32.3 @@ -29,7 +29,7 @@
    32.4    "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
    32.5  
    32.6  declare
    32.7 -  Mempty_def[code func del] single_def[code func del]
    32.8 +  Mempty_def[code del] single_def[code del]
    32.9  
   32.10  definition
   32.11    count :: "'a multiset => 'a => nat" where
   32.12 @@ -59,7 +59,7 @@
   32.13  begin
   32.14  
   32.15  definition
   32.16 -  union_def[code func del]:
   32.17 +  union_def[code del]:
   32.18    "M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
   32.19  
   32.20  definition
   32.21 @@ -69,7 +69,7 @@
   32.22    Zero_multiset_def [simp]: "0 = {#}"
   32.23  
   32.24  definition
   32.25 -  size_def[code func del]: "size M = setsum (count M) (set_of M)"
   32.26 +  size_def[code del]: "size M = setsum (count M) (set_of M)"
   32.27  
   32.28  instance ..
   32.29  
   32.30 @@ -207,10 +207,10 @@
   32.31  
   32.32  subsubsection {* Size *}
   32.33  
   32.34 -lemma size_empty [simp,code func]: "size {#} = 0"
   32.35 +lemma size_empty [simp,code]: "size {#} = 0"
   32.36  by (simp add: size_def)
   32.37  
   32.38 -lemma size_single [simp,code func]: "size {#b#} = 1"
   32.39 +lemma size_single [simp,code]: "size {#b#} = 1"
   32.40  by (simp add: size_def)
   32.41  
   32.42  lemma finite_set_of [iff]: "finite (set_of M)"
   32.43 @@ -223,7 +223,7 @@
   32.44  apply (simp add: Int_insert_left set_of_def)
   32.45  done
   32.46  
   32.47 -lemma size_union[simp,code func]: "size (M + N::'a multiset) = size M + size N"
   32.48 +lemma size_union[simp,code]: "size (M + N::'a multiset) = size M + size N"
   32.49  apply (unfold size_def)
   32.50  apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
   32.51   prefer 2
   32.52 @@ -376,16 +376,16 @@
   32.53  
   32.54  subsubsection {* Comprehension (filter) *}
   32.55  
   32.56 -lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}"
   32.57 +lemma MCollect_empty[simp, code]: "MCollect {#} P = {#}"
   32.58  by (simp add: MCollect_def Mempty_def Abs_multiset_inject
   32.59      in_multiset expand_fun_eq)
   32.60  
   32.61 -lemma MCollect_single[simp, code func]:
   32.62 +lemma MCollect_single[simp, code]:
   32.63    "MCollect {#x#} P = (if P x then {#x#} else {#})"
   32.64  by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
   32.65      in_multiset expand_fun_eq)
   32.66  
   32.67 -lemma MCollect_union[simp, code func]:
   32.68 +lemma MCollect_union[simp, code]:
   32.69    "MCollect (M+N) f = MCollect M f + MCollect N f"
   32.70  by (simp add: MCollect_def union_def Abs_multiset_inject
   32.71      in_multiset expand_fun_eq)
   32.72 @@ -500,7 +500,7 @@
   32.73  
   32.74  definition
   32.75    mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   32.76 -  [code func del]:"mult1 r =
   32.77 +  [code del]:"mult1 r =
   32.78      {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
   32.79        (\<forall>b. b :# K --> (b, a) \<in> r)}"
   32.80  
   32.81 @@ -716,10 +716,10 @@
   32.82  begin
   32.83  
   32.84  definition
   32.85 -  less_multiset_def [code func del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
   32.86 +  less_multiset_def [code del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
   32.87  
   32.88  definition
   32.89 -  le_multiset_def [code func del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
   32.90 +  le_multiset_def [code del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
   32.91  
   32.92  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
   32.93  unfolding trans_def by (blast intro: order_less_trans)
   32.94 @@ -983,11 +983,11 @@
   32.95  
   32.96  definition
   32.97    mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
   32.98 -  [code func del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
   32.99 +  [code del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
  32.100  
  32.101  definition
  32.102    mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
  32.103 -  [code func del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
  32.104 +  [code del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
  32.105  
  32.106  notation mset_le  (infix "\<subseteq>#" 50)
  32.107  notation mset_less  (infix "\<subset>#" 50)
  32.108 @@ -1448,22 +1448,22 @@
  32.109  
  32.110  subsection {* Image *}
  32.111  
  32.112 -definition [code func del]: "image_mset f == fold_mset (op + o single o f) {#}"
  32.113 +definition [code del]: "image_mset f == fold_mset (op + o single o f) {#}"
  32.114  
  32.115  interpretation image_left_comm: left_commutative ["op + o single o f"]
  32.116  by (unfold_locales) (simp add:union_ac)
  32.117  
  32.118 -lemma image_mset_empty [simp, code func]: "image_mset f {#} = {#}"
  32.119 +lemma image_mset_empty [simp, code]: "image_mset f {#} = {#}"
  32.120  by (simp add: image_mset_def)
  32.121  
  32.122 -lemma image_mset_single [simp, code func]: "image_mset f {#x#} = {#f x#}"
  32.123 +lemma image_mset_single [simp, code]: "image_mset f {#x#} = {#f x#}"
  32.124  by (simp add: image_mset_def)
  32.125  
  32.126  lemma image_mset_insert:
  32.127    "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
  32.128  by (simp add: image_mset_def add_ac)
  32.129  
  32.130 -lemma image_mset_union[simp, code func]:
  32.131 +lemma image_mset_union[simp, code]:
  32.132    "image_mset f (M+N) = image_mset f M + image_mset f N"
  32.133  apply (induct N)
  32.134   apply simp
    33.1 --- a/src/HOL/Library/Nat_Infinity.thy	Fri Oct 10 06:45:50 2008 +0200
    33.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Fri Oct 10 06:45:53 2008 +0200
    33.3 @@ -37,7 +37,7 @@
    33.4    [code inline]: "1 = Fin 1"
    33.5  
    33.6  definition
    33.7 -  [code inline, code func del]: "number_of k = Fin (number_of k)"
    33.8 +  [code inline, code del]: "number_of k = Fin (number_of k)"
    33.9  
   33.10  instance ..
   33.11  
    34.1 --- a/src/HOL/Library/Nested_Environment.thy	Fri Oct 10 06:45:50 2008 +0200
    34.2 +++ b/src/HOL/Library/Nested_Environment.thy	Fri Oct 10 06:45:53 2008 +0200
    34.3 @@ -525,11 +525,11 @@
    34.4  
    34.5  text {* Environments and code generation *}
    34.6  
    34.7 -lemma [code func, code func del]:
    34.8 +lemma [code, code del]:
    34.9    fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
   34.10    shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
   34.11  
   34.12 -lemma eq_env_code [code func]:
   34.13 +lemma eq_env_code [code]:
   34.14    fixes x y :: "'a\<Colon>eq"
   34.15      and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
   34.16    shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
   34.17 @@ -567,7 +567,7 @@
   34.18            of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
   34.19  qed simp_all
   34.20  
   34.21 -lemma [code func, code func del]:
   34.22 +lemma [code, code del]:
   34.23    "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
   34.24  
   34.25  end
    35.1 --- a/src/HOL/Library/Option_ord.thy	Fri Oct 10 06:45:50 2008 +0200
    35.2 +++ b/src/HOL/Library/Option_ord.thy	Fri Oct 10 06:45:53 2008 +0200
    35.3 @@ -13,10 +13,10 @@
    35.4  begin
    35.5  
    35.6  definition less_eq_option where
    35.7 -  [code func del]: "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
    35.8 +  [code del]: "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
    35.9  
   35.10  definition less_option where
   35.11 -  [code func del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
   35.12 +  [code del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
   35.13  
   35.14  lemma less_eq_option_None [simp]: "None \<le> x"
   35.15    by (simp add: less_eq_option_def)
    36.1 --- a/src/HOL/Library/Primes.thy	Fri Oct 10 06:45:50 2008 +0200
    36.2 +++ b/src/HOL/Library/Primes.thy	Fri Oct 10 06:45:53 2008 +0200
    36.3 @@ -16,7 +16,7 @@
    36.4  
    36.5  definition
    36.6    prime :: "nat \<Rightarrow> bool" where
    36.7 -  [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    36.8 +  [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    36.9  
   36.10  
   36.11  lemma two_is_prime: "prime 2"
    37.1 --- a/src/HOL/Library/Product_ord.thy	Fri Oct 10 06:45:50 2008 +0200
    37.2 +++ b/src/HOL/Library/Product_ord.thy	Fri Oct 10 06:45:53 2008 +0200
    37.3 @@ -13,16 +13,16 @@
    37.4  begin
    37.5  
    37.6  definition
    37.7 -  prod_le_def [code func del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
    37.8 +  prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
    37.9  
   37.10  definition
   37.11 -  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
   37.12 +  prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
   37.13  
   37.14  instance ..
   37.15  
   37.16  end
   37.17  
   37.18 -lemma [code func]:
   37.19 +lemma [code]:
   37.20    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   37.21    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   37.22    unfolding prod_le_def prod_less_def by simp_all
    38.1 --- a/src/HOL/Library/RType.thy	Fri Oct 10 06:45:50 2008 +0200
    38.2 +++ b/src/HOL/Library/RType.thy	Fri Oct 10 06:45:53 2008 +0200
    38.3 @@ -89,7 +89,7 @@
    38.4    #> TypedefPackage.interpretation Typerep.perhaps_add_def
    38.5  *}
    38.6  
    38.7 -lemma [code func]:
    38.8 +lemma [code]:
    38.9    "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
   38.10       \<and> list_all2 eq_class.eq tys1 tys2"
   38.11    by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
    39.1 --- a/src/HOL/Library/Ref.thy	Fri Oct 10 06:45:50 2008 +0200
    39.2 +++ b/src/HOL/Library/Ref.thy	Fri Oct 10 06:45:53 2008 +0200
    39.3 @@ -51,7 +51,7 @@
    39.4    by (cases f)
    39.5      (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
    39.6  
    39.7 -lemma update_change [code func]:
    39.8 +lemma update_change [code]:
    39.9    "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
   39.10    by (auto simp add: monad_simp change_def lookup_chain)
   39.11  
    40.1 --- a/src/HOL/Library/Sublist_Order.thy	Fri Oct 10 06:45:50 2008 +0200
    40.2 +++ b/src/HOL/Library/Sublist_Order.thy	Fri Oct 10 06:45:53 2008 +0200
    40.3 @@ -47,7 +47,7 @@
    40.4    using assms by (induct rule: less_eq_list.induct) blast+
    40.5  
    40.6  definition
    40.7 -  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    40.8 +  [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    40.9  
   40.10  lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
   40.11    by (induct rule: ileq_induct) auto
    41.1 --- a/src/HOL/Library/Univ_Poly.thy	Fri Oct 10 06:45:50 2008 +0200
    41.2 +++ b/src/HOL/Library/Univ_Poly.thy	Fri Oct 10 06:45:53 2008 +0200
    41.3 @@ -72,7 +72,7 @@
    41.4  
    41.5  definition (in semiring_0)
    41.6    divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "divides" 70) where
    41.7 -  [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
    41.8 +  [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
    41.9  
   41.10      --{*order of a polynomial*}
   41.11  definition (in ring_1) order :: "'a => 'a list => nat" where
    42.1 --- a/src/HOL/Library/Word.thy	Fri Oct 10 06:45:50 2008 +0200
    42.2 +++ b/src/HOL/Library/Word.thy	Fri Oct 10 06:45:53 2008 +0200
    42.3 @@ -2042,7 +2042,7 @@
    42.4  
    42.5  definition
    42.6    length_nat :: "nat => nat" where
    42.7 -  [code func del]: "length_nat x = (LEAST n. x < 2 ^ n)"
    42.8 +  [code del]: "length_nat x = (LEAST n. x < 2 ^ n)"
    42.9  
   42.10  lemma length_nat: "length (nat_to_bv n) = length_nat n"
   42.11    apply (simp add: length_nat_def)
   42.12 @@ -2267,7 +2267,7 @@
   42.13    fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
   42.14      fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
   42.15  
   42.16 -declare fast_bv_to_nat_helper.simps [code func del]
   42.17 +declare fast_bv_to_nat_helper.simps [code del]
   42.18  
   42.19  lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
   42.20      fast_bv_to_nat_helper bs (Int.Bit0 bin)"
    43.1 --- a/src/HOL/List.thy	Fri Oct 10 06:45:50 2008 +0200
    43.2 +++ b/src/HOL/List.thy	Fri Oct 10 06:45:53 2008 +0200
    43.3 @@ -204,7 +204,7 @@
    43.4  
    43.5  definition
    43.6    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
    43.7 -  [code func del]: "list_all2 P xs ys =
    43.8 +  [code del]: "list_all2 P xs ys =
    43.9      (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
   43.10  
   43.11  definition
   43.12 @@ -2872,7 +2872,7 @@
   43.13  
   43.14  definition
   43.15   sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
   43.16 - [code func del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
   43.17 + [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
   43.18  
   43.19  lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
   43.20    set(sorted_list_of_set A) = A &
   43.21 @@ -3057,7 +3057,7 @@
   43.22  constdefs
   43.23    set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
   43.24    "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
   43.25 -declare set_Cons_def [code func del]
   43.26 +declare set_Cons_def [code del]
   43.27  
   43.28  lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
   43.29  by (auto simp add: set_Cons_def)
   43.30 @@ -3095,7 +3095,7 @@
   43.31      "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
   43.32          --{*Compares lists by their length and then lexicographically*}
   43.33  
   43.34 -declare lex_def [code func del]
   43.35 +declare lex_def [code del]
   43.36  
   43.37  
   43.38  lemma wf_lexn: "wf r ==> wf (lexn r n)"
   43.39 @@ -3171,7 +3171,7 @@
   43.40    lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
   43.41    "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
   43.42              (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
   43.43 -declare lexord_def [code func del]
   43.44 +declare lexord_def [code del]
   43.45  
   43.46  lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
   43.47  by (unfold lexord_def, induct_tac y, auto) 
   43.48 @@ -3379,7 +3379,7 @@
   43.49  primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
   43.50    "nibble_pair_of_char (Char n m) = (n, m)"
   43.51  
   43.52 -declare nibble_pair_of_char.simps [code func del]
   43.53 +declare nibble_pair_of_char.simps [code del]
   43.54  
   43.55  setup {*
   43.56  let
   43.57 @@ -3393,11 +3393,11 @@
   43.58  end
   43.59  *}
   43.60  
   43.61 -lemma char_case_nibble_pair [code func, code inline]:
   43.62 +lemma char_case_nibble_pair [code, code inline]:
   43.63    "char_case f = split f o nibble_pair_of_char"
   43.64    by (simp add: expand_fun_eq split: char.split)
   43.65  
   43.66 -lemma char_rec_nibble_pair [code func, code inline]:
   43.67 +lemma char_rec_nibble_pair [code, code inline]:
   43.68    "char_rec f = split f o nibble_pair_of_char"
   43.69    unfolding char_case_nibble_pair [symmetric]
   43.70    by (simp add: expand_fun_eq split: char.split)
    44.1 --- a/src/HOL/Map.thy	Fri Oct 10 06:45:50 2008 +0200
    44.2 +++ b/src/HOL/Map.thy	Fri Oct 10 06:45:53 2008 +0200
    44.3 @@ -91,7 +91,7 @@
    44.4    by simp_all
    44.5  
    44.6  defs
    44.7 -  map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    44.8 +  map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    44.9  
   44.10  
   44.11  subsection {* @{term [source] empty} *}
    45.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Oct 10 06:45:50 2008 +0200
    45.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Oct 10 06:45:53 2008 +0200
    45.3 @@ -768,7 +768,7 @@
    45.4  instantiation matrix :: (zero) zero
    45.5  begin
    45.6  
    45.7 -definition zero_matrix_def [code func del]: "0 = Abs_matrix (\<lambda>j i. 0)"
    45.8 +definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
    45.9  
   45.10  instance ..
   45.11  
   45.12 @@ -1440,9 +1440,9 @@
   45.13  instantiation matrix :: ("{lattice, zero}") lattice
   45.14  begin
   45.15  
   45.16 -definition [code func del]: "inf = combine_matrix inf"
   45.17 +definition [code del]: "inf = combine_matrix inf"
   45.18  
   45.19 -definition [code func del]: "sup = combine_matrix sup"
   45.20 +definition [code del]: "sup = combine_matrix sup"
   45.21  
   45.22  instance
   45.23    by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
   45.24 @@ -1453,7 +1453,7 @@
   45.25  begin
   45.26  
   45.27  definition
   45.28 -  plus_matrix_def [code func del]: "A + B = combine_matrix (op +) A B"
   45.29 +  plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
   45.30  
   45.31  instance ..
   45.32  
   45.33 @@ -1463,7 +1463,7 @@
   45.34  begin
   45.35  
   45.36  definition
   45.37 -  minus_matrix_def [code func del]: "- A = apply_matrix uminus A"
   45.38 +  minus_matrix_def [code del]: "- A = apply_matrix uminus A"
   45.39  
   45.40  instance ..
   45.41  
   45.42 @@ -1473,7 +1473,7 @@
   45.43  begin
   45.44  
   45.45  definition
   45.46 -  diff_matrix_def [code func del]: "A - B = combine_matrix (op -) A B"
   45.47 +  diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
   45.48  
   45.49  instance ..
   45.50  
   45.51 @@ -1483,7 +1483,7 @@
   45.52  begin
   45.53  
   45.54  definition
   45.55 -  times_matrix_def [code func del]: "A * B = mult_matrix (op *) (op +) A B"
   45.56 +  times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
   45.57  
   45.58  instance ..
   45.59  
   45.60 @@ -1493,7 +1493,7 @@
   45.61  begin
   45.62  
   45.63  definition
   45.64 -  abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
   45.65 +  abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
   45.66  
   45.67  instance ..
   45.68  
    46.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Fri Oct 10 06:45:50 2008 +0200
    46.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Oct 10 06:45:53 2008 +0200
    46.3 @@ -25,7 +25,7 @@
    46.4  lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0"
    46.5    by (simp add: sparse_row_matrix_def)
    46.6  
    46.7 -lemmas [code func] = sparse_row_vector_empty [symmetric]
    46.8 +lemmas [code] = sparse_row_vector_empty [symmetric]
    46.9  
   46.10  lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> ! x y. (foldl f (g x y) l = g x (foldl f y l))"
   46.11    by (induct l, auto)
   46.12 @@ -417,8 +417,8 @@
   46.13    apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
   46.14    done
   46.15  
   46.16 -lemmas [code func] = sparse_row_add_spmat [symmetric]
   46.17 -lemmas [code func] = sparse_row_vector_add [symmetric]
   46.18 +lemmas [code] = sparse_row_add_spmat [symmetric]
   46.19 +lemmas [code] = sparse_row_vector_add [symmetric]
   46.20  
   46.21  lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
   46.22    proof - 
    47.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 10 06:45:50 2008 +0200
    47.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 10 06:45:53 2008 +0200
    47.3 @@ -68,7 +68,7 @@
    47.4  definition
    47.5    "wf_class G = wfP ((subcls1 G)^--1)"
    47.6  
    47.7 -lemma class_rec_func (*[code func]*):
    47.8 +lemma class_rec_func (*[code]*):
    47.9    "class_rec G C t f = (if wf_class G then
   47.10      (case class G C
   47.11        of None \<Rightarrow> undefined
    48.1 --- a/src/HOL/NSA/HDeriv.thy	Fri Oct 10 06:45:50 2008 +0200
    48.2 +++ b/src/HOL/NSA/HDeriv.thy	Fri Oct 10 06:45:53 2008 +0200
    48.3 @@ -27,7 +27,7 @@
    48.4  
    48.5  definition
    48.6    increment :: "[real=>real,real,hypreal] => hypreal" where
    48.7 -  [code func del]: "increment f x h = (@inc. f NSdifferentiable x &
    48.8 +  [code del]: "increment f x h = (@inc. f NSdifferentiable x &
    48.9             inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
   48.10  
   48.11  
    49.1 --- a/src/HOL/NSA/HLim.thy	Fri Oct 10 06:45:50 2008 +0200
    49.2 +++ b/src/HOL/NSA/HLim.thy	Fri Oct 10 06:45:53 2008 +0200
    49.3 @@ -16,18 +16,18 @@
    49.4  definition
    49.5    NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
    49.6              ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
    49.7 -  [code func del]: "f -- a --NS> L =
    49.8 +  [code del]: "f -- a --NS> L =
    49.9      (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
   49.10  
   49.11  definition
   49.12    isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
   49.13      --{*NS definition dispenses with limit notions*}
   49.14 -  [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
   49.15 +  [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
   49.16           ( *f* f) y @= star_of (f a))"
   49.17  
   49.18  definition
   49.19    isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
   49.20 -  [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
   49.21 +  [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
   49.22  
   49.23  
   49.24  subsection {* Limits of Functions *}
    50.1 --- a/src/HOL/NSA/HLog.thy	Fri Oct 10 06:45:50 2008 +0200
    50.2 +++ b/src/HOL/NSA/HLog.thy	Fri Oct 10 06:45:53 2008 +0200
    50.3 @@ -20,11 +20,11 @@
    50.4  
    50.5  definition
    50.6    powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
    50.7 -  [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
    50.8 +  [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
    50.9    
   50.10  definition
   50.11    hlog :: "[hypreal,hypreal] => hypreal" where
   50.12 -  [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
   50.13 +  [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
   50.14  
   50.15  lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
   50.16  by (simp add: powhr_def starfun2_star_n)
    51.1 --- a/src/HOL/NSA/HSEQ.thy	Fri Oct 10 06:45:50 2008 +0200
    51.2 +++ b/src/HOL/NSA/HSEQ.thy	Fri Oct 10 06:45:53 2008 +0200
    51.3 @@ -16,7 +16,7 @@
    51.4    NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
    51.5      ("((_)/ ----NS> (_))" [60, 60] 60) where
    51.6      --{*Nonstandard definition of convergence of sequence*}
    51.7 -  [code func del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    51.8 +  [code del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    51.9  
   51.10  definition
   51.11    nslim :: "(nat => 'a::real_normed_vector) => 'a" where
   51.12 @@ -31,12 +31,12 @@
   51.13  definition
   51.14    NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
   51.15      --{*Nonstandard definition for bounded sequence*}
   51.16 -  [code func del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
   51.17 +  [code del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
   51.18  
   51.19  definition
   51.20    NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
   51.21      --{*Nonstandard definition*}
   51.22 -  [code func del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
   51.23 +  [code del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
   51.24  
   51.25  subsection {* Limits of Sequences *}
   51.26  
    52.1 --- a/src/HOL/NSA/HSeries.thy	Fri Oct 10 06:45:50 2008 +0200
    52.2 +++ b/src/HOL/NSA/HSeries.thy	Fri Oct 10 06:45:53 2008 +0200
    52.3 @@ -13,7 +13,7 @@
    52.4  
    52.5  definition
    52.6    sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
    52.7 -  [code func del]: "sumhr = 
    52.8 +  [code del]: "sumhr = 
    52.9        (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
   52.10  
   52.11  definition
   52.12 @@ -22,7 +22,7 @@
   52.13  
   52.14  definition
   52.15    NSsummable :: "(nat=>real) => bool" where
   52.16 -  [code func del]: "NSsummable f = (\<exists>s. f NSsums s)"
   52.17 +  [code del]: "NSsummable f = (\<exists>s. f NSsums s)"
   52.18  
   52.19  definition
   52.20    NSsuminf   :: "(nat=>real) => real" where
    53.1 --- a/src/HOL/NSA/HyperDef.thy	Fri Oct 10 06:45:50 2008 +0200
    53.2 +++ b/src/HOL/NSA/HyperDef.thy	Fri Oct 10 06:45:53 2008 +0200
    53.3 @@ -47,7 +47,7 @@
    53.4  begin
    53.5  
    53.6  definition
    53.7 -  star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)"
    53.8 +  star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)"
    53.9  
   53.10  instance ..
   53.11  
   53.12 @@ -113,7 +113,7 @@
   53.13  
   53.14  definition
   53.15    of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
   53.16 -  [transfer_unfold, code func del]: "of_hypreal = *f* of_real"
   53.17 +  [transfer_unfold, code del]: "of_hypreal = *f* of_real"
   53.18  
   53.19  lemma Standard_of_hypreal [simp]:
   53.20    "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
   53.21 @@ -428,7 +428,7 @@
   53.22  subsection{*Powers with Hypernatural Exponents*}
   53.23  
   53.24  definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
   53.25 -  hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N"
   53.26 +  hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
   53.27    (* hypernatural powers of hyperreals *)
   53.28  
   53.29  lemma Standard_hyperpow [simp]:
    54.1 --- a/src/HOL/NSA/HyperNat.thy	Fri Oct 10 06:45:50 2008 +0200
    54.2 +++ b/src/HOL/NSA/HyperNat.thy	Fri Oct 10 06:45:53 2008 +0200
    54.3 @@ -19,7 +19,7 @@
    54.4  
    54.5  definition
    54.6    hSuc :: "hypnat => hypnat" where
    54.7 -  hSuc_def [transfer_unfold, code func del]: "hSuc = *f* Suc"
    54.8 +  hSuc_def [transfer_unfold, code del]: "hSuc = *f* Suc"
    54.9  
   54.10  subsection{*Properties Transferred from Naturals*}
   54.11  
   54.12 @@ -367,7 +367,7 @@
   54.13  
   54.14  definition
   54.15    of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
   54.16 -  of_hypnat_def [transfer_unfold, code func del]: "of_hypnat = *f* of_nat"
   54.17 +  of_hypnat_def [transfer_unfold, code del]: "of_hypnat = *f* of_nat"
   54.18  
   54.19  lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
   54.20  by transfer (rule of_nat_0)
    55.1 --- a/src/HOL/NSA/NSA.thy	Fri Oct 10 06:45:50 2008 +0200
    55.2 +++ b/src/HOL/NSA/NSA.thy	Fri Oct 10 06:45:53 2008 +0200
    55.3 @@ -17,15 +17,15 @@
    55.4  
    55.5  definition
    55.6    Infinitesimal  :: "('a::real_normed_vector) star set" where
    55.7 -  [code func del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
    55.8 +  [code del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
    55.9  
   55.10  definition
   55.11    HFinite :: "('a::real_normed_vector) star set" where
   55.12 -  [code func del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
   55.13 +  [code del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
   55.14  
   55.15  definition
   55.16    HInfinite :: "('a::real_normed_vector) star set" where
   55.17 -  [code func del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
   55.18 +  [code del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
   55.19  
   55.20  definition
   55.21    approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "@=" 50) where
   55.22 @@ -58,7 +58,7 @@
   55.23  
   55.24  definition
   55.25    scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
   55.26 -  [transfer_unfold, code func del]: "scaleHR = starfun2 scaleR"
   55.27 +  [transfer_unfold, code del]: "scaleHR = starfun2 scaleR"
   55.28  
   55.29  lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
   55.30  by (simp add: hnorm_def)
    56.1 --- a/src/HOL/NSA/NSCA.thy	Fri Oct 10 06:45:50 2008 +0200
    56.2 +++ b/src/HOL/NSA/NSCA.thy	Fri Oct 10 06:45:53 2008 +0200
    56.3 @@ -16,7 +16,7 @@
    56.4  
    56.5  definition --{* standard part map*}
    56.6    stc :: "hcomplex => hcomplex" where 
    56.7 -  [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
    56.8 +  [code del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
    56.9  
   56.10  
   56.11  subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
    57.1 --- a/src/HOL/NSA/NSComplex.thy	Fri Oct 10 06:45:50 2008 +0200
    57.2 +++ b/src/HOL/NSA/NSComplex.thy	Fri Oct 10 06:45:53 2008 +0200
    57.3 @@ -26,11 +26,11 @@
    57.4  
    57.5  definition
    57.6    hRe :: "hcomplex => hypreal" where
    57.7 -  [code func del]: "hRe = *f* Re"
    57.8 +  [code del]: "hRe = *f* Re"
    57.9  
   57.10  definition
   57.11    hIm :: "hcomplex => hypreal" where
   57.12 -  [code func del]: "hIm = *f* Im"
   57.13 +  [code del]: "hIm = *f* Im"
   57.14  
   57.15  
   57.16    (*------ imaginary unit ----------*)
   57.17 @@ -43,22 +43,22 @@
   57.18  
   57.19  definition
   57.20    hcnj :: "hcomplex => hcomplex" where
   57.21 -  [code func del]: "hcnj = *f* cnj"
   57.22 +  [code del]: "hcnj = *f* cnj"
   57.23  
   57.24    (*------------ Argand -------------*)
   57.25  
   57.26  definition
   57.27    hsgn :: "hcomplex => hcomplex" where
   57.28 -  [code func del]: "hsgn = *f* sgn"
   57.29 +  [code del]: "hsgn = *f* sgn"
   57.30  
   57.31  definition
   57.32    harg :: "hcomplex => hypreal" where
   57.33 -  [code func del]: "harg = *f* arg"
   57.34 +  [code del]: "harg = *f* arg"
   57.35  
   57.36  definition
   57.37    (* abbreviation for (cos a + i sin a) *)
   57.38    hcis :: "hypreal => hcomplex" where
   57.39 -  [code func del]:"hcis = *f* cis"
   57.40 +  [code del]:"hcis = *f* cis"
   57.41  
   57.42    (*----- injection from hyperreals -----*)
   57.43  
   57.44 @@ -69,16 +69,16 @@
   57.45  definition
   57.46    (* abbreviation for r*(cos a + i sin a) *)
   57.47    hrcis :: "[hypreal, hypreal] => hcomplex" where
   57.48 -  [code func del]: "hrcis = *f2* rcis"
   57.49 +  [code del]: "hrcis = *f2* rcis"
   57.50  
   57.51    (*------------ e ^ (x + iy) ------------*)
   57.52  definition
   57.53    hexpi :: "hcomplex => hcomplex" where
   57.54 -  [code func del]: "hexpi = *f* expi"
   57.55 +  [code del]: "hexpi = *f* expi"
   57.56  
   57.57  definition
   57.58    HComplex :: "[hypreal,hypreal] => hcomplex" where
   57.59 -  [code func del]: "HComplex = *f2* Complex"
   57.60 +  [code del]: "HComplex = *f2* Complex"
   57.61  
   57.62  lemmas hcomplex_defs [transfer_unfold] =
   57.63    hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
    58.1 --- a/src/HOL/NSA/Star.thy	Fri Oct 10 06:45:50 2008 +0200
    58.2 +++ b/src/HOL/NSA/Star.thy	Fri Oct 10 06:45:53 2008 +0200
    58.3 @@ -17,12 +17,12 @@
    58.4  
    58.5  definition
    58.6    InternalSets :: "'a star set set" where
    58.7 -  [code func del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
    58.8 +  [code del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
    58.9  
   58.10  definition
   58.11    (* nonstandard extension of function *)
   58.12    is_starext  :: "['a star => 'a star, 'a => 'a] => bool" where
   58.13 -  [code func del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
   58.14 +  [code del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
   58.15                          ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
   58.16  
   58.17  definition
   58.18 @@ -32,7 +32,7 @@
   58.19  
   58.20  definition
   58.21    InternalFuns :: "('a star => 'b star) set" where
   58.22 -  [code func del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
   58.23 +  [code del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
   58.24  
   58.25  
   58.26  (*--------------------------------------------------------
    59.1 --- a/src/HOL/NSA/StarDef.thy	Fri Oct 10 06:45:50 2008 +0200
    59.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Oct 10 06:45:53 2008 +0200
    59.3 @@ -291,7 +291,7 @@
    59.4  subsection {* Internal predicates *}
    59.5  
    59.6  definition unstar :: "bool star \<Rightarrow> bool" where
    59.7 -  [code func del]: "unstar b \<longleftrightarrow> b = star_of True"
    59.8 +  [code del]: "unstar b \<longleftrightarrow> b = star_of True"
    59.9  
   59.10  lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
   59.11  by (simp add: unstar_def star_of_def star_n_eq_iff)
   59.12 @@ -432,7 +432,7 @@
   59.13  begin
   59.14  
   59.15  definition
   59.16 -  star_zero_def [code func del]:    "0 \<equiv> star_of 0"
   59.17 +  star_zero_def [code del]:    "0 \<equiv> star_of 0"
   59.18  
   59.19  instance ..
   59.20  
   59.21 @@ -442,7 +442,7 @@
   59.22  begin
   59.23  
   59.24  definition
   59.25 -  star_one_def [code func del]:     "1 \<equiv> star_of 1"
   59.26 +  star_one_def [code del]:     "1 \<equiv> star_of 1"
   59.27  
   59.28  instance ..
   59.29  
   59.30 @@ -452,7 +452,7 @@
   59.31  begin
   59.32  
   59.33  definition
   59.34 -  star_add_def [code func del]:     "(op +) \<equiv> *f2* (op +)"
   59.35 +  star_add_def [code del]:     "(op +) \<equiv> *f2* (op +)"
   59.36  
   59.37  instance ..
   59.38  
   59.39 @@ -462,7 +462,7 @@
   59.40  begin
   59.41  
   59.42  definition
   59.43 -  star_mult_def [code func del]:    "(op *) \<equiv> *f2* (op *)"
   59.44 +  star_mult_def [code del]:    "(op *) \<equiv> *f2* (op *)"
   59.45  
   59.46  instance ..
   59.47  
   59.48 @@ -472,7 +472,7 @@
   59.49  begin
   59.50  
   59.51  definition
   59.52 -  star_minus_def [code func del]:   "uminus \<equiv> *f* uminus"
   59.53 +  star_minus_def [code del]:   "uminus \<equiv> *f* uminus"
   59.54  
   59.55  instance ..
   59.56  
   59.57 @@ -482,7 +482,7 @@
   59.58  begin
   59.59  
   59.60  definition
   59.61 -  star_diff_def [code func del]:    "(op -) \<equiv> *f2* (op -)"
   59.62 +  star_diff_def [code del]:    "(op -) \<equiv> *f2* (op -)"
   59.63  
   59.64  instance ..
   59.65  
    60.1 --- a/src/HOL/Nat.thy	Fri Oct 10 06:45:50 2008 +0200
    60.2 +++ b/src/HOL/Nat.thy	Fri Oct 10 06:45:53 2008 +0200
    60.3 @@ -55,7 +55,7 @@
    60.4  instantiation nat :: zero
    60.5  begin
    60.6  
    60.7 -definition Zero_nat_def [code func del]:
    60.8 +definition Zero_nat_def [code del]:
    60.9    "0 = Abs_Nat Zero_Rep"
   60.10  
   60.11  instance ..
   60.12 @@ -1281,7 +1281,7 @@
   60.13  
   60.14  definition
   60.15    Nats  :: "'a set" where
   60.16 -  [code func del]: "Nats = range of_nat"
   60.17 +  [code del]: "Nats = range of_nat"
   60.18  
   60.19  notation (xsymbols)
   60.20    Nats  ("\<nat>")
    61.1 --- a/src/HOL/NatBin.thy	Fri Oct 10 06:45:50 2008 +0200
    61.2 +++ b/src/HOL/NatBin.thy	Fri Oct 10 06:45:53 2008 +0200
    61.3 @@ -18,7 +18,7 @@
    61.4  begin
    61.5  
    61.6  definition
    61.7 -  nat_number_of_def [code inline, code func del]: "number_of v = nat (number_of v)"
    61.8 +  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
    61.9  
   61.10  instance ..
   61.11  
    62.1 --- a/src/HOL/Orderings.thy	Fri Oct 10 06:45:50 2008 +0200
    62.2 +++ b/src/HOL/Orderings.thy	Fri Oct 10 06:45:53 2008 +0200
    62.3 @@ -968,10 +968,10 @@
    62.4  begin
    62.5  
    62.6  definition
    62.7 -  le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
    62.8 +  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
    62.9  
   62.10  definition
   62.11 -  less_bool_def [code func del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
   62.12 +  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
   62.13  
   62.14  instance
   62.15    by intro_classes (auto simp add: le_bool_def less_bool_def)
   62.16 @@ -990,7 +990,7 @@
   62.17  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
   62.18  by (simp add: le_bool_def)
   62.19  
   62.20 -lemma [code func]:
   62.21 +lemma [code]:
   62.22    "False \<le> b \<longleftrightarrow> True"
   62.23    "True \<le> b \<longleftrightarrow> b"
   62.24    "False < b \<longleftrightarrow> b"
   62.25 @@ -1004,10 +1004,10 @@
   62.26  begin
   62.27  
   62.28  definition
   62.29 -  le_fun_def [code func del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
   62.30 +  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
   62.31  
   62.32  definition
   62.33 -  less_fun_def [code func del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
   62.34 +  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
   62.35  
   62.36  instance ..
   62.37  
    63.1 --- a/src/HOL/Product_Type.thy	Fri Oct 10 06:45:50 2008 +0200
    63.2 +++ b/src/HOL/Product_Type.thy	Fri Oct 10 06:45:53 2008 +0200
    63.3 @@ -23,10 +23,10 @@
    63.4    -- "prefer plain propositional version"
    63.5  
    63.6  lemma
    63.7 -  shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
    63.8 -    and [code func]: "eq_class.eq True P \<longleftrightarrow> P" 
    63.9 -    and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
   63.10 -    and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
   63.11 +  shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
   63.12 +    and [code]: "eq_class.eq True P \<longleftrightarrow> P" 
   63.13 +    and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
   63.14 +    and [code]: "eq_class.eq P True \<longleftrightarrow> P"
   63.15      and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
   63.16    by (simp_all add: eq)
   63.17  
   63.18 @@ -89,7 +89,7 @@
   63.19  
   63.20  instance unit :: eq ..
   63.21  
   63.22 -lemma [code func]:
   63.23 +lemma [code]:
   63.24    "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
   63.25  
   63.26  code_type unit
   63.27 @@ -359,10 +359,10 @@
   63.28  
   63.29  subsubsection {* @{text split} and @{text curry} *}
   63.30  
   63.31 -lemma split_conv [simp, code func]: "split f (a, b) = f a b"
   63.32 +lemma split_conv [simp, code]: "split f (a, b) = f a b"
   63.33    by (simp add: split_def)
   63.34  
   63.35 -lemma curry_conv [simp, code func]: "curry f a b = f (a, b)"
   63.36 +lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
   63.37    by (simp add: curry_def)
   63.38  
   63.39  lemmas split = split_conv  -- {* for backwards compatibility *}
   63.40 @@ -728,9 +728,9 @@
   63.41  *}
   63.42  
   63.43  definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   63.44 -  [code func del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
   63.45 +  [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
   63.46  
   63.47 -lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
   63.48 +lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
   63.49    by (simp add: prod_fun_def)
   63.50  
   63.51  lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
   63.52 @@ -758,12 +758,12 @@
   63.53  definition
   63.54    apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
   63.55  where
   63.56 -  [code func del]: "apfst f = prod_fun f id"
   63.57 +  [code del]: "apfst f = prod_fun f id"
   63.58  
   63.59  definition
   63.60    apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
   63.61  where
   63.62 -  [code func del]: "apsnd f = prod_fun id f"
   63.63 +  [code del]: "apsnd f = prod_fun id f"
   63.64  
   63.65  lemma apfst_conv [simp, code]:
   63.66    "apfst f (x, y) = (f x, y)" 
   63.67 @@ -917,7 +917,7 @@
   63.68  
   63.69  instance * :: (eq, eq) eq ..
   63.70  
   63.71 -lemma [code func]:
   63.72 +lemma [code]:
   63.73    "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
   63.74  
   63.75  lemma split_case_cert:
    64.1 --- a/src/HOL/Real/ContNotDenum.thy	Fri Oct 10 06:45:50 2008 +0200
    64.2 +++ b/src/HOL/Real/ContNotDenum.thy	Fri Oct 10 06:45:53 2008 +0200
    64.3 @@ -403,7 +403,7 @@
    64.4         (f (Suc n)) \<notin> e)
    64.5        )"
    64.6  
    64.7 -declare newInt.simps [code func del]
    64.8 +declare newInt.simps [code del]
    64.9  
   64.10  subsubsection {* Properties *}
   64.11  
    65.1 --- a/src/HOL/Real/PReal.thy	Fri Oct 10 06:45:50 2008 +0200
    65.2 +++ b/src/HOL/Real/PReal.thy	Fri Oct 10 06:45:53 2008 +0200
    65.3 @@ -19,7 +19,7 @@
    65.4  
    65.5  definition
    65.6    cut :: "rat set => bool" where
    65.7 -  [code func del]: "cut A = ({} \<subset> A &
    65.8 +  [code del]: "cut A = ({} \<subset> A &
    65.9              A < {r. 0 < r} &
   65.10              (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
   65.11  
   65.12 @@ -56,7 +56,7 @@
   65.13  
   65.14  definition
   65.15    diff_set :: "[rat set,rat set] => rat set" where
   65.16 -  [code func del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
   65.17 +  [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
   65.18  
   65.19  definition
   65.20    mult_set :: "[rat set,rat set] => rat set" where
   65.21 @@ -64,17 +64,17 @@
   65.22  
   65.23  definition
   65.24    inverse_set :: "rat set => rat set" where
   65.25 -  [code func del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
   65.26 +  [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
   65.27  
   65.28  instantiation preal :: "{ord, plus, minus, times, inverse, one}"
   65.29  begin
   65.30  
   65.31  definition
   65.32 -  preal_less_def [code func del]:
   65.33 +  preal_less_def [code del]:
   65.34      "R < S == Rep_preal R < Rep_preal S"
   65.35  
   65.36  definition
   65.37 -  preal_le_def [code func del]:
   65.38 +  preal_le_def [code del]:
   65.39      "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
   65.40  
   65.41  definition
    66.1 --- a/src/HOL/Real/RComplete.thy	Fri Oct 10 06:45:50 2008 +0200
    66.2 +++ b/src/HOL/Real/RComplete.thy	Fri Oct 10 06:45:53 2008 +0200
    66.3 @@ -488,7 +488,7 @@
    66.4  
    66.5  definition
    66.6    floor :: "real => int" where
    66.7 -  [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
    66.8 +  [code del]: "floor r = (LEAST n::int. r < real (n+1))"
    66.9  
   66.10  definition
   66.11    ceiling :: "real => int" where
    67.1 --- a/src/HOL/Real/Rational.thy	Fri Oct 10 06:45:50 2008 +0200
    67.2 +++ b/src/HOL/Real/Rational.thy	Fri Oct 10 06:45:53 2008 +0200
    67.3 @@ -71,7 +71,7 @@
    67.4  
    67.5  definition
    67.6    Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
    67.7 -  [code func del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
    67.8 +  [code del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
    67.9  
   67.10  code_datatype Fract
   67.11  
   67.12 @@ -101,7 +101,7 @@
   67.13    One_rat_def [code, code unfold]: "1 = Fract 1 1"
   67.14  
   67.15  definition
   67.16 -  add_rat_def [code func del]:
   67.17 +  add_rat_def [code del]:
   67.18    "q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   67.19      ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
   67.20  
   67.21 @@ -116,7 +116,7 @@
   67.22  qed
   67.23  
   67.24  definition
   67.25 -  minus_rat_def [code func del]:
   67.26 +  minus_rat_def [code del]:
   67.27    "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {(- fst x, snd x)})"
   67.28  
   67.29  lemma minus_rat [simp, code]: "- Fract a b = Fract (- a) b"
   67.30 @@ -130,7 +130,7 @@
   67.31    by (cases "b = 0") (simp_all add: eq_rat)
   67.32  
   67.33  definition
   67.34 -  diff_rat_def [code func del]: "q - r = q + - (r::rat)"
   67.35 +  diff_rat_def [code del]: "q - r = q + - (r::rat)"
   67.36  
   67.37  lemma diff_rat [simp]:
   67.38    assumes "b \<noteq> 0" and "d \<noteq> 0"
   67.39 @@ -138,7 +138,7 @@
   67.40    using assms by (simp add: diff_rat_def)
   67.41  
   67.42  definition
   67.43 -  mult_rat_def [code func del]:
   67.44 +  mult_rat_def [code del]:
   67.45    "q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   67.46      ratrel``{(fst x * fst y, snd x * snd y)})"
   67.47  
   67.48 @@ -219,7 +219,7 @@
   67.49  begin
   67.50  
   67.51  definition
   67.52 -  rat_number_of_def [code func del]: "number_of w = Fract w 1"
   67.53 +  rat_number_of_def [code del]: "number_of w = Fract w 1"
   67.54  
   67.55  instance by intro_classes (simp add: rat_number_of_def of_int_rat)
   67.56  
   67.57 @@ -265,7 +265,7 @@
   67.58  begin
   67.59  
   67.60  definition
   67.61 -  inverse_rat_def [code func del]:
   67.62 +  inverse_rat_def [code del]:
   67.63    "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q.
   67.64       ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
   67.65  
   67.66 @@ -277,7 +277,7 @@
   67.67  qed
   67.68  
   67.69  definition
   67.70 -  divide_rat_def [code func del]: "q / r = q * inverse (r::rat)"
   67.71 +  divide_rat_def [code del]: "q / r = q * inverse (r::rat)"
   67.72  
   67.73  lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   67.74    by (simp add: divide_rat_def)
   67.75 @@ -320,7 +320,7 @@
   67.76  begin
   67.77  
   67.78  definition
   67.79 -  le_rat_def [code func del]:
   67.80 +  le_rat_def [code del]:
   67.81     "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
   67.82        {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
   67.83  
   67.84 @@ -370,7 +370,7 @@
   67.85  qed
   67.86  
   67.87  definition
   67.88 -  less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
   67.89 +  less_rat_def [code del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
   67.90  
   67.91  lemma less_rat [simp]:
   67.92    assumes "b \<noteq> 0" and "d \<noteq> 0"
   67.93 @@ -450,13 +450,13 @@
   67.94  begin
   67.95  
   67.96  definition
   67.97 -  abs_rat_def [code func del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
   67.98 +  abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
   67.99  
  67.100  lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
  67.101    by (auto simp add: abs_rat_def zabs_def Zero_rat_def less_rat not_less le_less minus_rat eq_rat zero_compare_simps)
  67.102  
  67.103  definition
  67.104 -  sgn_rat_def [code func del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
  67.105 +  sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
  67.106  
  67.107  lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)"
  67.108    unfolding Fract_of_int_eq
  67.109 @@ -553,7 +553,7 @@
  67.110  begin
  67.111  
  67.112  definition of_rat :: "rat \<Rightarrow> 'a" where
  67.113 -  [code func del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
  67.114 +  [code del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
  67.115  
  67.116  end
  67.117  
  67.118 @@ -680,7 +680,7 @@
  67.119  
  67.120  definition
  67.121    Rats  :: "'a set" where
  67.122 -  [code func del]: "Rats = range of_rat"
  67.123 +  [code del]: "Rats = range of_rat"
  67.124  
  67.125  notation (xsymbols)
  67.126    Rats  ("\<rat>")
  67.127 @@ -850,9 +850,9 @@
  67.128  qed
  67.129  
  67.130  definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
  67.131 -  [simp, code func del]: "Fract_norm a b = Fract a b"
  67.132 +  [simp, code del]: "Fract_norm a b = Fract a b"
  67.133  
  67.134 -lemma [code func]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
  67.135 +lemma [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
  67.136    if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
  67.137    by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
  67.138  
  67.139 @@ -863,7 +863,7 @@
  67.140  instantiation rat :: eq
  67.141  begin
  67.142  
  67.143 -definition [code func del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0"
  67.144 +definition [code del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0"
  67.145  
  67.146  instance by default (simp add: eq_rat_def)
  67.147  
    68.1 --- a/src/HOL/Real/RealDef.thy	Fri Oct 10 06:45:50 2008 +0200
    68.2 +++ b/src/HOL/Real/RealDef.thy	Fri Oct 10 06:45:53 2008 +0200
    68.3 @@ -15,7 +15,7 @@
    68.4  
    68.5  definition
    68.6    realrel   ::  "((preal * preal) * (preal * preal)) set" where
    68.7 -  [code func del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    68.8 +  [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    68.9  
   68.10  typedef (Real)  real = "UNIV//realrel"
   68.11    by (auto simp add: quotient_def)
   68.12 @@ -23,46 +23,46 @@
   68.13  definition
   68.14    (** these don't use the overloaded "real" function: users don't see them **)
   68.15    real_of_preal :: "preal => real" where
   68.16 -  [code func del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
   68.17 +  [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
   68.18  
   68.19  instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
   68.20  begin
   68.21  
   68.22  definition
   68.23 -  real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
   68.24 +  real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
   68.25  
   68.26  definition
   68.27 -  real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
   68.28 +  real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
   68.29  
   68.30  definition
   68.31 -  real_add_def [code func del]: "z + w =
   68.32 +  real_add_def [code del]: "z + w =
   68.33         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
   68.34                   { Abs_Real(realrel``{(x+u, y+v)}) })"
   68.35  
   68.36  definition
   68.37 -  real_minus_def [code func del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   68.38 +  real_minus_def [code del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   68.39  
   68.40  definition
   68.41 -  real_diff_def [code func del]: "r - (s::real) = r + - s"
   68.42 +  real_diff_def [code del]: "r - (s::real) = r + - s"
   68.43  
   68.44  definition
   68.45 -  real_mult_def [code func del]:
   68.46 +  real_mult_def [code del]:
   68.47      "z * w =
   68.48         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
   68.49                   { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
   68.50  
   68.51  definition
   68.52 -  real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
   68.53 +  real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
   68.54  
   68.55  definition
   68.56 -  real_divide_def [code func del]: "R / (S::real) = R * inverse S"
   68.57 +  real_divide_def [code del]: "R / (S::real) = R * inverse S"
   68.58  
   68.59  definition
   68.60 -  real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
   68.61 +  real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
   68.62      (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
   68.63  
   68.64  definition
   68.65 -  real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   68.66 +  real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   68.67  
   68.68  definition
   68.69    real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
   68.70 @@ -939,7 +939,7 @@
   68.71  begin
   68.72  
   68.73  definition
   68.74 -  real_number_of_def [code func del]: "number_of w = real_of_int w"
   68.75 +  real_number_of_def [code del]: "number_of w = real_of_int w"
   68.76  
   68.77  instance
   68.78    by intro_classes (simp add: real_number_of_def)
    69.1 --- a/src/HOL/Real/RealVector.thy	Fri Oct 10 06:45:50 2008 +0200
    69.2 +++ b/src/HOL/Real/RealVector.thy	Fri Oct 10 06:45:53 2008 +0200
    69.3 @@ -308,7 +308,7 @@
    69.4  
    69.5  definition
    69.6    Reals :: "'a::real_algebra_1 set" where
    69.7 -  [code func del]: "Reals \<equiv> range of_real"
    69.8 +  [code del]: "Reals \<equiv> range of_real"
    69.9  
   69.10  notation (xsymbols)
   69.11    Reals  ("\<real>")
    70.1 --- a/src/HOL/Set.thy	Fri Oct 10 06:45:50 2008 +0200
    70.2 +++ b/src/HOL/Set.thy	Fri Oct 10 06:45:53 2008 +0200
    70.3 @@ -324,8 +324,8 @@
    70.4  text {* Isomorphisms between predicates and sets. *}
    70.5  
    70.6  defs
    70.7 -  mem_def [code func]: "x : S == S x"
    70.8 -  Collect_def [code func]: "Collect P == P"
    70.9 +  mem_def [code]: "x : S == S x"
   70.10 +  Collect_def [code]: "Collect P == P"
   70.11  
   70.12  defs
   70.13    Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   70.14 @@ -2061,7 +2061,7 @@
   70.15  
   70.16  constdefs
   70.17    vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
   70.18 -  [code func del]: "f -` B == {x. f x : B}"
   70.19 +  [code del]: "f -` B == {x. f x : B}"
   70.20  
   70.21  
   70.22  subsubsection {* Basic rules *}
   70.23 @@ -2156,7 +2156,7 @@
   70.24  definition
   70.25    contents :: "'a set \<Rightarrow> 'a"
   70.26  where
   70.27 -  [code func del]: "contents X = (THE x. X = {x})"
   70.28 +  [code del]: "contents X = (THE x. X = {x})"
   70.29  
   70.30  lemma contents_eq [simp]: "contents {x} = x"
   70.31    by (simp add: contents_def)
   70.32 @@ -2189,22 +2189,22 @@
   70.33  
   70.34  subsection {* Rudimentary code generation *}
   70.35  
   70.36 -lemma empty_code [code func]: "{} x \<longleftrightarrow> False"
   70.37 +lemma empty_code [code]: "{} x \<longleftrightarrow> False"
   70.38    unfolding empty_def Collect_def ..
   70.39  
   70.40 -lemma UNIV_code [code func]: "UNIV x \<longleftrightarrow> True"
   70.41 +lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
   70.42    unfolding UNIV_def Collect_def ..
   70.43  
   70.44 -lemma insert_code [code func]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
   70.45 +lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
   70.46    unfolding insert_def Collect_def mem_def Un_def by auto
   70.47  
   70.48 -lemma inter_code [code func]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
   70.49 +lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
   70.50    unfolding Int_def Collect_def mem_def ..
   70.51  
   70.52 -lemma union_code [code func]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
   70.53 +lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
   70.54    unfolding Un_def Collect_def mem_def ..
   70.55  
   70.56 -lemma vimage_code [code func]: "(f -` A) x = A (f x)"
   70.57 +lemma vimage_code [code]: "(f -` A) x = A (f x)"
   70.58    unfolding vimage_def Collect_def mem_def ..
   70.59  
   70.60  
    71.1 --- a/src/HOL/SizeChange/Graphs.thy	Fri Oct 10 06:45:50 2008 +0200
    71.2 +++ b/src/HOL/SizeChange/Graphs.thy	Fri Oct 10 06:45:53 2008 +0200
    71.3 @@ -67,7 +67,7 @@
    71.4    graph_zero_def: "0 = Graph {}" 
    71.5  
    71.6  definition
    71.7 -  graph_plus_def [code func del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
    71.8 +  graph_plus_def [code del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
    71.9  
   71.10  instance proof
   71.11    fix x y z :: "('a,'b) graph"
   71.12 @@ -83,22 +83,22 @@
   71.13  begin
   71.14  
   71.15  definition
   71.16 -  graph_leq_def [code func del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
   71.17 +  graph_leq_def [code del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
   71.18  
   71.19  definition
   71.20 -  graph_less_def [code func del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
   71.21 +  graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
   71.22  
   71.23  definition
   71.24 -  [code func del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
   71.25 +  [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
   71.26  
   71.27  definition
   71.28 -  [code func del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
   71.29 +  [code del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
   71.30  
   71.31  definition
   71.32 -  Inf_graph_def [code func del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
   71.33 +  Inf_graph_def [code del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
   71.34  
   71.35  definition
   71.36 -  Sup_graph_def [code func del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
   71.37 +  Sup_graph_def [code del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
   71.38  
   71.39  instance proof
   71.40    fix x y z :: "('a,'b) graph"
   71.41 @@ -165,7 +165,7 @@
   71.42  begin
   71.43  
   71.44  definition
   71.45 -  graph_mult_def [code func del]: "G * H = grcomp G H" 
   71.46 +  graph_mult_def [code del]: "G * H = grcomp G H" 
   71.47  
   71.48  instance proof
   71.49    fix a :: "('a, 'b) graph"
    72.1 --- a/src/HOL/SizeChange/Implementation.thy	Fri Oct 10 06:45:50 2008 +0200
    72.2 +++ b/src/HOL/SizeChange/Implementation.thy	Fri Oct 10 06:45:53 2008 +0200
    72.3 @@ -122,16 +122,16 @@
    72.4  code_modulename SML
    72.5    Implementation Graphs
    72.6  
    72.7 -lemma [code func]:
    72.8 +lemma [code]:
    72.9    "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
   72.10    "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
   72.11    unfolding graph_leq_def graph_less_def by rule+
   72.12  
   72.13 -lemma [code func]:
   72.14 +lemma [code]:
   72.15    "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
   72.16    unfolding graph_plus_def ..
   72.17  
   72.18 -lemma [code func]:
   72.19 +lemma [code]:
   72.20    "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
   72.21    unfolding graph_mult_def ..
   72.22  
    73.1 --- a/src/HOL/Tools/ComputeHOL.thy	Fri Oct 10 06:45:50 2008 +0200
    73.2 +++ b/src/HOL/Tools/ComputeHOL.thy	Fri Oct 10 06:45:53 2008 +0200
    73.3 @@ -1,5 +1,5 @@
    73.4  theory ComputeHOL
    73.5 -imports Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
    73.6 +imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
    73.7  begin
    73.8  
    73.9  lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)
    74.1 --- a/src/HOL/Wellfounded.thy	Fri Oct 10 06:45:50 2008 +0200
    74.2 +++ b/src/HOL/Wellfounded.thy	Fri Oct 10 06:45:53 2008 +0200
    74.3 @@ -40,7 +40,7 @@
    74.4       (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    74.5  
    74.6    wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
    74.7 -  [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    74.8 +  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    74.9  
   74.10  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   74.11    "acyclicP r == acyclic {(x, y). r x y}"
   74.12 @@ -840,10 +840,10 @@
   74.13  
   74.14  setup Size.setup
   74.15  
   74.16 -lemma size_bool [code func]:
   74.17 +lemma size_bool [code]:
   74.18    "size (b\<Colon>bool) = 0" by (cases b) auto
   74.19  
   74.20 -lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
   74.21 +lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
   74.22    by (induct n) simp_all
   74.23  
   74.24  declare "prod.size" [noatp]
    75.1 --- a/src/HOL/Word/BinGeneral.thy	Fri Oct 10 06:45:50 2008 +0200
    75.2 +++ b/src/HOL/Word/BinGeneral.thy	Fri Oct 10 06:45:53 2008 +0200
    75.3 @@ -129,7 +129,7 @@
    75.4  subsection {* Destructors for binary integers *}
    75.5  
    75.6  definition bin_rl :: "int \<Rightarrow> int \<times> bit" where 
    75.7 -  [code func del]: "bin_rl w = (THE (r, l). w = r BIT l)"
    75.8 +  [code del]: "bin_rl w = (THE (r, l). w = r BIT l)"
    75.9  
   75.10  lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
   75.11    apply (unfold bin_rl_def)
   75.12 @@ -139,10 +139,10 @@
   75.13    done
   75.14  
   75.15  definition
   75.16 -  bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
   75.17 +  bin_rest_def [code del]: "bin_rest w = fst (bin_rl w)"
   75.18  
   75.19  definition
   75.20 -  bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
   75.21 +  bin_last_def [code del] : "bin_last w = snd (bin_rl w)"
   75.22  
   75.23  primrec bin_nth where
   75.24    Z: "bin_nth w 0 = (bin_last w = bit.B1)"
   75.25 @@ -159,7 +159,7 @@
   75.26    "bin_rl (r BIT b) = (r, b)"
   75.27    unfolding bin_rl_char by simp_all
   75.28  
   75.29 -declare bin_rl_simps(1-4) [code func]
   75.30 +declare bin_rl_simps(1-4) [code]
   75.31  
   75.32  lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
   75.33  
   75.34 @@ -212,7 +212,7 @@
   75.35    "bin_rest (w BIT b) = w"
   75.36    unfolding bin_rest_def by auto
   75.37  
   75.38 -declare bin_rest_simps(1-4) [code func]
   75.39 +declare bin_rest_simps(1-4) [code]
   75.40  
   75.41  lemma bin_last_simps [simp]: 
   75.42    "bin_last Int.Pls = bit.B0"
   75.43 @@ -222,7 +222,7 @@
   75.44    "bin_last (w BIT b) = b"
   75.45    unfolding bin_last_def by auto
   75.46  
   75.47 -declare bin_last_simps(1-4) [code func]
   75.48 +declare bin_last_simps(1-4) [code]
   75.49  
   75.50  lemma bin_r_l_extras [simp]:
   75.51    "bin_last 0 = bit.B0"
   75.52 @@ -403,7 +403,7 @@
   75.53  subsection {* Truncating binary integers *}
   75.54  
   75.55  definition
   75.56 -  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
   75.57 +  bin_sign_def [code del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
   75.58  
   75.59  lemma bin_sign_simps [simp]:
   75.60    "bin_sign Int.Pls = Int.Pls"
   75.61 @@ -413,7 +413,7 @@
   75.62    "bin_sign (w BIT b) = bin_sign w"
   75.63    unfolding bin_sign_def by (auto simp: bin_rec_simps)
   75.64  
   75.65 -declare bin_sign_simps(1-4) [code func]
   75.66 +declare bin_sign_simps(1-4) [code]
   75.67  
   75.68  lemma bin_sign_rest [simp]: 
   75.69    "bin_sign (bin_rest w) = (bin_sign w)"
    76.1 --- a/src/HOL/Word/BinOperations.thy	Fri Oct 10 06:45:50 2008 +0200
    76.2 +++ b/src/HOL/Word/BinOperations.thy	Fri Oct 10 06:45:53 2008 +0200
    76.3 @@ -21,19 +21,19 @@
    76.4  begin
    76.5  
    76.6  definition
    76.7 -  int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls 
    76.8 +  int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls 
    76.9      (\<lambda>w b s. s BIT (NOT b))"
   76.10  
   76.11  definition
   76.12 -  int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
   76.13 +  int_and_def [code del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
   76.14      (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
   76.15  
   76.16  definition
   76.17 -  int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
   76.18 +  int_or_def [code del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
   76.19      (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
   76.20  
   76.21  definition
   76.22 -  int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
   76.23 +  int_xor_def [code del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
   76.24      (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
   76.25  
   76.26  instance ..
   76.27 @@ -48,13 +48,13 @@
   76.28    "NOT (w BIT b) = (NOT w) BIT (NOT b)"
   76.29    unfolding int_not_def by (simp_all add: bin_rec_simps)
   76.30  
   76.31 -declare int_not_simps(1-4) [code func]
   76.32 +declare int_not_simps(1-4) [code]
   76.33  
   76.34 -lemma int_xor_Pls [simp, code func]: 
   76.35 +lemma int_xor_Pls [simp, code]: 
   76.36    "Int.Pls XOR x = x"
   76.37    unfolding int_xor_def by (simp add: bin_rec_PM)
   76.38  
   76.39 -lemma int_xor_Min [simp, code func]: 
   76.40 +lemma int_xor_Min [simp, code]: 
   76.41    "Int.Min XOR x = NOT x"
   76.42    unfolding int_xor_def by (simp add: bin_rec_PM)
   76.43  
   76.44 @@ -69,7 +69,7 @@
   76.45    apply (simp add: int_not_simps [symmetric])
   76.46    done
   76.47  
   76.48 -lemma int_xor_Bits2 [simp, code func]: 
   76.49 +lemma int_xor_Bits2 [simp, code]: 
   76.50    "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
   76.51    "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
   76.52    "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
   76.53 @@ -85,16 +85,16 @@
   76.54     apply clarsimp+
   76.55    done
   76.56  
   76.57 -lemma int_xor_extra_simps [simp, code func]:
   76.58 +lemma int_xor_extra_simps [simp, code]:
   76.59    "w XOR Int.Pls = w"
   76.60    "w XOR Int.Min = NOT w"
   76.61    using int_xor_x_simps' by simp_all
   76.62  
   76.63 -lemma int_or_Pls [simp, code func]: 
   76.64 +lemma int_or_Pls [simp, code]: 
   76.65    "Int.Pls OR x = x"
   76.66    by (unfold int_or_def) (simp add: bin_rec_PM)
   76.67    
   76.68 -lemma int_or_Min [simp, code func]:
   76.69 +lemma int_or_Min [simp, code]:
   76.70    "Int.Min OR x = Int.Min"
   76.71    by (unfold int_or_def) (simp add: bin_rec_PM)
   76.72  
   76.73 @@ -102,7 +102,7 @@
   76.74    "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
   76.75    unfolding int_or_def by (simp add: bin_rec_simps)
   76.76  
   76.77 -lemma int_or_Bits2 [simp, code func]: 
   76.78 +lemma int_or_Bits2 [simp, code]: 
   76.79    "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
   76.80    "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   76.81    "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
   76.82 @@ -118,16 +118,16 @@
   76.83     apply clarsimp+
   76.84    done
   76.85  
   76.86 -lemma int_or_extra_simps [simp, code func]:
   76.87 +lemma int_or_extra_simps [simp, code]:
   76.88    "w OR Int.Pls = w"
   76.89    "w OR Int.Min = Int.Min"
   76.90    using int_or_x_simps' by simp_all
   76.91  
   76.92 -lemma int_and_Pls [simp, code func]:
   76.93 +lemma int_and_Pls [simp, code]:
   76.94    "Int.Pls AND x = Int.Pls"
   76.95    unfolding int_and_def by (simp add: bin_rec_PM)
   76.96  
   76.97 -lemma int_and_Min [simp, code func]:
   76.98 +lemma int_and_Min [simp, code]:
   76.99    "Int.Min AND x = x"
  76.100    unfolding int_and_def by (simp add: bin_rec_PM)
  76.101  
  76.102 @@ -135,7 +135,7 @@
  76.103    "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
  76.104    unfolding int_and_def by (simp add: bin_rec_simps)
  76.105  
  76.106 -lemma int_and_Bits2 [simp, code func]: 
  76.107 +lemma int_and_Bits2 [simp, code]: 
  76.108    "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
  76.109    "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
  76.110    "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
  76.111 @@ -151,7 +151,7 @@
  76.112     apply clarsimp+
  76.113    done
  76.114  
  76.115 -lemma int_and_extra_simps [simp, code func]:
  76.116 +lemma int_and_extra_simps [simp, code]:
  76.117    "w AND Int.Pls = Int.Pls"
  76.118    "w AND Int.Min = w"
  76.119    using int_and_x_simps' by simp_all
    77.1 --- a/src/HOL/Word/WordDefinition.thy	Fri Oct 10 06:45:50 2008 +0200
    77.2 +++ b/src/HOL/Word/WordDefinition.thy	Fri Oct 10 06:45:53 2008 +0200
    77.3 @@ -30,7 +30,7 @@
    77.4          only difference in these is the type class *}
    77.5    word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
    77.6  where
    77.7 -  [code func del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
    77.8 +  [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
    77.9  
   77.10  code_datatype word_of_int
   77.11  
   77.12 @@ -96,9 +96,9 @@
   77.13  
   77.14  subsection  "Arithmetic operations"
   77.15  
   77.16 -declare uint_def [code func del]
   77.17 +declare uint_def [code del]
   77.18  
   77.19 -lemma [code func]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
   77.20 +lemma [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
   77.21    by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse)
   77.22      (insert range_bintrunc, auto)
   77.23  
    78.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy	Fri Oct 10 06:45:50 2008 +0200
    78.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy	Fri Oct 10 06:45:53 2008 +0200
    78.3 @@ -9,7 +9,7 @@
    78.4  imports ExecutableContent Code_Char Efficient_Nat
    78.5  begin
    78.6  
    78.7 -declare isnorm.simps [code func del]
    78.8 +declare isnorm.simps [code del]
    78.9  
   78.10  ML {* (*FIXME get rid of this*)
   78.11  nonfix union;
    79.1 --- a/src/HOL/ex/NormalForm.thy	Fri Oct 10 06:45:50 2008 +0200
    79.2 +++ b/src/HOL/ex/NormalForm.thy	Fri Oct 10 06:45:53 2008 +0200
    79.3 @@ -12,7 +12,7 @@
    79.4  lemma "p \<longrightarrow> True" by normalization
    79.5  declare disj_assoc [code nbe]
    79.6  lemma "((P | Q) | R) = (P | (Q | R))" by normalization
    79.7 -declare disj_assoc [code func del]
    79.8 +declare disj_assoc [code del]
    79.9  lemma "0 + (n::nat) = n" by normalization
   79.10  lemma "0 + Suc n = Suc n" by normalization
   79.11  lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
    80.1 --- a/src/HOL/ex/Numeral.thy	Fri Oct 10 06:45:50 2008 +0200
    80.2 +++ b/src/HOL/ex/Numeral.thy	Fri Oct 10 06:45:53 2008 +0200
    80.3 @@ -74,19 +74,19 @@
    80.4  begin
    80.5  
    80.6  definition one_num :: num where
    80.7 -  [code func del]: "1 = num_of_nat 1"
    80.8 +  [code del]: "1 = num_of_nat 1"
    80.9  
   80.10  definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
   80.11 -  [code func del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
   80.12 +  [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
   80.13  
   80.14  definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
   80.15 -  [code func del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
   80.16 +  [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
   80.17  
   80.18  definition Dig0 :: "num \<Rightarrow> num" where
   80.19 -  [code func del]: "Dig0 n = n + n"
   80.20 +  [code del]: "Dig0 n = n + n"
   80.21  
   80.22  definition Dig1 :: "num \<Rightarrow> num" where
   80.23 -  [code func del]: "Dig1 n = n + n + 1"
   80.24 +  [code del]: "Dig1 n = n + n + 1"
   80.25  
   80.26  instance proof
   80.27  qed (simp_all add: one_num_def plus_num_def times_num_def
   80.28 @@ -503,10 +503,10 @@
   80.29  begin
   80.30  
   80.31  definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
   80.32 -  [code func del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
   80.33 +  [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
   80.34  
   80.35  definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
   80.36 -  [code func del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
   80.37 +  [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
   80.38  
   80.39  instance proof
   80.40  qed (auto simp add: less_eq_num_def less_num_def
   80.41 @@ -768,10 +768,10 @@
   80.42  lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
   80.43  
   80.44  definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   80.45 -  [simp, code func del]: "sub m n = (of_num m - of_num n)"
   80.46 +  [simp, code del]: "sub m n = (of_num m - of_num n)"
   80.47  
   80.48  definition dup :: "int \<Rightarrow> int" where
   80.49 -  [code func del]: "dup k = 2 * k"
   80.50 +  [code del]: "dup k = 2 * k"
   80.51  
   80.52  lemma Dig_sub [code]:
   80.53    "sub 1 1 = 0"
   80.54 @@ -794,7 +794,7 @@
   80.55    "dup (Mns n) = Mns (Dig0 n)"
   80.56    by (simp_all add: dup_def of_num.simps)
   80.57    
   80.58 -lemma [code func, code func del]:
   80.59 +lemma [code, code del]:
   80.60    "(1 :: int) = 1"
   80.61    "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
   80.62    "(uminus :: int \<Rightarrow> int) = uminus"
    81.1 --- a/src/HOL/ex/Random.thy	Fri Oct 10 06:45:50 2008 +0200
    81.2 +++ b/src/HOL/ex/Random.thy	Fri Oct 10 06:45:53 2008 +0200
    81.3 @@ -124,7 +124,7 @@
    81.4  definition
    81.5    select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
    81.6  where
    81.7 -  [code func del]: "select_default k x y = (do
    81.8 +  [code del]: "select_default k x y = (do
    81.9       l \<leftarrow> range k;
   81.10       return (if l + 1 < k then x else y)
   81.11     done)"
    82.1 --- a/src/Pure/Isar/code.ML	Fri Oct 10 06:45:50 2008 +0200
    82.2 +++ b/src/Pure/Isar/code.ML	Fri Oct 10 06:45:53 2008 +0200
    82.3 @@ -96,12 +96,10 @@
    82.4  
    82.5  fun add_attribute (attr as (name, _)) =
    82.6    let
    82.7 -    fun add_parser ("", parser) attrs = attrs @ [("", parser)]
    82.8 +    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
    82.9        | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
   82.10 -    fun error "" = error ("Code attribute already declared")
   82.11 -      | error name = error ("Code attribute " ^ name ^ " already declared")
   82.12 -  in CodeAttr.map (fn attrs => if AList.defined (op =) attrs name
   82.13 -    then error name else add_parser attr attrs)
   82.14 +  in CodeAttr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
   82.15 +    then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
   82.16    end;
   82.17  
   82.18  val _ =
   82.19 @@ -637,7 +635,7 @@
   82.20          || Scan.succeed (mk_attribute add))
   82.21    in
   82.22      TypeInterpretation.init
   82.23 -    #> add_del_attribute ("func", (add_eqn, del_eqn))
   82.24 +    #> add_del_attribute ("", (add_eqn, del_eqn))
   82.25      #> add_simple_attribute ("nbe", add_nonlinear_eqn)
   82.26      #> add_del_attribute ("inline", (add_inline, del_inline))
   82.27      #> add_del_attribute ("post", (add_post, del_post))