code attributes use common underscore convention
authorhaftmann
Tue Jul 14 10:54:04 2009 +0200 (2009-07-14)
changeset 319982c7a24f74db9
parent 31997 de0d280c31a7
child 31999 cb1f26c0de5b
code attributes use common underscore convention
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
src/HOL/Code_Eval.thy
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/HOL.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/Library/Code_Char_chr.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Float.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Polynomial.thy
src/HOL/List.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/Nat.thy
src/HOL/Nat_Numeral.thy
src/HOL/Option.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/Rational.thy
src/HOL/RealDef.thy
src/HOL/SetInterval.thy
src/HOL/String.thy
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/ex/Numeral.thy
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -1190,7 +1190,13 @@
     1.4      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     1.5      ;
     1.6  
     1.7 -    'code' ( 'inline' ) ? ( 'del' ) ?
     1.8 +    'code' ( 'del' ) ?
     1.9 +    ;
    1.10 +
    1.11 +    'code_unfold' ( 'del' ) ?
    1.12 +    ;
    1.13 +
    1.14 +    'code_post' ( 'del' ) ?
    1.15      ;
    1.16    \end{rail}
    1.17  
    1.18 @@ -1280,11 +1286,15 @@
    1.19    generation.  Usually packages introducing code equations provide
    1.20    a reasonable default setup for selection.
    1.21  
    1.22 -  \item @{attribute (HOL) code}~@{text inline} declares (or with
    1.23 +  \item @{attribute (HOL) code_inline} declares (or with
    1.24    option ``@{text "del"}'' removes) inlining theorems which are
    1.25    applied as rewrite rules to any code equation during
    1.26    preprocessing.
    1.27  
    1.28 +  \item @{attribute (HOL) code_post} declares (or with
    1.29 +  option ``@{text "del"}'' removes) theorems which are
    1.30 +  applied as rewrite rules to any result of an evaluation.
    1.31 +
    1.32    \item @{command (HOL) "print_codesetup"} gives an overview on
    1.33    selected code equations and code generator datatypes.
    1.34  
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jul 14 10:53:44 2009 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jul 14 10:54:04 2009 +0200
     2.3 @@ -1201,7 +1201,13 @@
     2.4      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     2.5      ;
     2.6  
     2.7 -    'code' ( 'inline' ) ? ( 'del' ) ?
     2.8 +    'code' ( 'del' ) ?
     2.9 +    ;
    2.10 +
    2.11 +    'code_unfold' ( 'del' ) ?
    2.12 +    ;
    2.13 +
    2.14 +    'code_post' ( 'del' ) ?
    2.15      ;
    2.16    \end{rail}
    2.17  
    2.18 @@ -1288,11 +1294,15 @@
    2.19    generation.  Usually packages introducing code equations provide
    2.20    a reasonable default setup for selection.
    2.21  
    2.22 -  \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
    2.23 +  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
    2.24    option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
    2.25    applied as rewrite rules to any code equation during
    2.26    preprocessing.
    2.27  
    2.28 +  \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
    2.29 +  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
    2.30 +  applied as rewrite rules to any result of an evaluation.
    2.31 +
    2.32    \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
    2.33    selected code equations and code generator datatypes.
    2.34  
     3.1 --- a/src/HOL/Code_Eval.thy	Tue Jul 14 10:53:44 2009 +0200
     3.2 +++ b/src/HOL/Code_Eval.thy	Tue Jul 14 10:54:04 2009 +0200
     3.3 @@ -32,7 +32,7 @@
     3.4    \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
     3.5    "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
     3.6  
     3.7 -lemma valapp_code [code, code inline]:
     3.8 +lemma valapp_code [code, code_inline]:
     3.9    "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    3.10    by (simp only: valapp_def fst_conv snd_conv)
    3.11  
     4.1 --- a/src/HOL/Code_Numeral.thy	Tue Jul 14 10:53:44 2009 +0200
     4.2 +++ b/src/HOL/Code_Numeral.thy	Tue Jul 14 10:54:04 2009 +0200
     4.3 @@ -176,16 +176,16 @@
     4.4  
     4.5  end
     4.6  
     4.7 -lemma zero_code_numeral_code [code inline, code]:
     4.8 +lemma zero_code_numeral_code [code_inline, code]:
     4.9    "(0\<Colon>code_numeral) = Numeral0"
    4.10    by (simp add: number_of_code_numeral_def Pls_def)
    4.11 -lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
    4.12 +lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
    4.13    using zero_code_numeral_code ..
    4.14  
    4.15 -lemma one_code_numeral_code [code inline, code]:
    4.16 +lemma one_code_numeral_code [code_inline, code]:
    4.17    "(1\<Colon>code_numeral) = Numeral1"
    4.18    by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
    4.19 -lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
    4.20 +lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
    4.21    using one_code_numeral_code ..
    4.22  
    4.23  lemma plus_code_numeral_code [code nbe]:
     5.1 --- a/src/HOL/Divides.thy	Tue Jul 14 10:53:44 2009 +0200
     5.2 +++ b/src/HOL/Divides.thy	Tue Jul 14 10:54:04 2009 +0200
     5.3 @@ -131,7 +131,7 @@
     5.4    note that ultimately show thesis by blast
     5.5  qed
     5.6  
     5.7 -lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
     5.8 +lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
     5.9  proof
    5.10    assume "b mod a = 0"
    5.11    with mod_div_equality [of b a] have "b div a * a = b" by simp
     6.1 --- a/src/HOL/HOL.thy	Tue Jul 14 10:53:44 2009 +0200
     6.2 +++ b/src/HOL/HOL.thy	Tue Jul 14 10:54:04 2009 +0200
     6.3 @@ -1787,7 +1787,7 @@
     6.4    assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
     6.5  begin
     6.6  
     6.7 -lemma eq [code unfold, code inline del]: "eq = (op =)"
     6.8 +lemma eq [code_unfold, code_inline del]: "eq = (op =)"
     6.9    by (rule ext eq_equals)+
    6.10  
    6.11  lemma eq_refl: "eq x x \<longleftrightarrow> True"
    6.12 @@ -1796,7 +1796,7 @@
    6.13  lemma equals_eq: "(op =) \<equiv> eq"
    6.14    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    6.15  
    6.16 -declare equals_eq [symmetric, code post]
    6.17 +declare equals_eq [symmetric, code_post]
    6.18  
    6.19  end
    6.20  
    6.21 @@ -1847,7 +1847,7 @@
    6.22  
    6.23  lemmas [code] = Let_def if_True if_False
    6.24  
    6.25 -lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
    6.26 +lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
    6.27  
    6.28  instantiation itself :: (type) eq
    6.29  begin
     7.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 14 10:53:44 2009 +0200
     7.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 14 10:54:04 2009 +0200
     7.3 @@ -283,7 +283,7 @@
     7.4  where
     7.5    [code del]: "raise_exc e = raise []"
     7.6  
     7.7 -lemma raise_raise_exc [code, code inline]:
     7.8 +lemma raise_raise_exc [code, code_inline]:
     7.9    "raise s = raise_exc (Fail (STR s))"
    7.10    unfolding Fail_def raise_exc_def raise_def ..
    7.11  
     8.1 --- a/src/HOL/Int.thy	Tue Jul 14 10:53:44 2009 +0200
     8.2 +++ b/src/HOL/Int.thy	Tue Jul 14 10:54:04 2009 +0200
     8.3 @@ -650,11 +650,11 @@
     8.4  
     8.5  text {* Removal of leading zeroes *}
     8.6  
     8.7 -lemma Bit0_Pls [simp, code post]:
     8.8 +lemma Bit0_Pls [simp, code_post]:
     8.9    "Bit0 Pls = Pls"
    8.10    unfolding numeral_simps by simp
    8.11  
    8.12 -lemma Bit1_Min [simp, code post]:
    8.13 +lemma Bit1_Min [simp, code_post]:
    8.14    "Bit1 Min = Min"
    8.15    unfolding numeral_simps by simp
    8.16  
    8.17 @@ -2126,11 +2126,11 @@
    8.18  
    8.19  hide (open) const nat_aux
    8.20  
    8.21 -lemma zero_is_num_zero [code, code inline, symmetric, code post]:
    8.22 +lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
    8.23    "(0\<Colon>int) = Numeral0" 
    8.24    by simp
    8.25  
    8.26 -lemma one_is_num_one [code, code inline, symmetric, code post]:
    8.27 +lemma one_is_num_one [code, code_inline, symmetric, code_post]:
    8.28    "(1\<Colon>int) = Numeral1" 
    8.29    by simp
    8.30  
     9.1 --- a/src/HOL/IntDiv.thy	Tue Jul 14 10:53:44 2009 +0200
     9.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 14 10:54:04 2009 +0200
     9.3 @@ -36,7 +36,7 @@
     9.4  
     9.5  text{*algorithm for the general case @{term "b\<noteq>0"}*}
     9.6  definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
     9.7 -  [code inline]: "negateSnd = apsnd uminus"
     9.8 +  [code_inline]: "negateSnd = apsnd uminus"
     9.9  
    9.10  definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    9.11      --{*The full division algorithm considers all possible signs for a, b
    10.1 --- a/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 10:53:44 2009 +0200
    10.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 10:54:04 2009 +0200
    10.3 @@ -24,11 +24,11 @@
    10.4  
    10.5  lemmas [code del] = char.recs char.cases char.size
    10.6  
    10.7 -lemma [code, code inline]:
    10.8 +lemma [code, code_inline]:
    10.9    "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
   10.10    by (cases c) (auto simp add: nibble_pair_of_nat_char)
   10.11  
   10.12 -lemma [code, code inline]:
   10.13 +lemma [code, code_inline]:
   10.14    "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
   10.15    by (cases c) (auto simp add: nibble_pair_of_nat_char)
   10.16  
    11.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 10:53:44 2009 +0200
    11.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 10:54:04 2009 +0200
    11.3 @@ -26,15 +26,15 @@
    11.4  
    11.5  code_datatype number_nat_inst.number_of_nat
    11.6  
    11.7 -lemma zero_nat_code [code, code inline]:
    11.8 +lemma zero_nat_code [code, code_inline]:
    11.9    "0 = (Numeral0 :: nat)"
   11.10    by simp
   11.11 -lemmas [code post] = zero_nat_code [symmetric]
   11.12 +lemmas [code_post] = zero_nat_code [symmetric]
   11.13  
   11.14 -lemma one_nat_code [code, code inline]:
   11.15 +lemma one_nat_code [code, code_inline]:
   11.16    "1 = (Numeral1 :: nat)"
   11.17    by simp
   11.18 -lemmas [code post] = one_nat_code [symmetric]
   11.19 +lemmas [code_post] = one_nat_code [symmetric]
   11.20  
   11.21  lemma Suc_code [code]:
   11.22    "Suc n = n + 1"
   11.23 @@ -89,7 +89,7 @@
   11.24    expression:
   11.25  *}
   11.26  
   11.27 -lemma [code, code unfold]:
   11.28 +lemma [code, code_unfold]:
   11.29    "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
   11.30    by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
   11.31  
   11.32 @@ -302,7 +302,7 @@
   11.33    Natural numerals.
   11.34  *}
   11.35  
   11.36 -lemma [code inline, symmetric, code post]:
   11.37 +lemma [code_inline, symmetric, code_post]:
   11.38    "nat (number_of i) = number_nat_inst.number_of_nat i"
   11.39    -- {* this interacts as desired with @{thm nat_number_of_def} *}
   11.40    by (simp add: number_nat_inst.number_of_nat)
   11.41 @@ -335,9 +335,9 @@
   11.42    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   11.43    unfolding nat_number_of_def number_of_is_id neg_def by simp
   11.44  
   11.45 -lemma of_nat_int [code unfold]:
   11.46 +lemma of_nat_int [code_unfold]:
   11.47    "of_nat = int" by (simp add: int_def)
   11.48 -declare of_nat_int [symmetric, code post]
   11.49 +declare of_nat_int [symmetric, code_post]
   11.50  
   11.51  code_const int
   11.52    (SML "_")
    12.1 --- a/src/HOL/Library/Executable_Set.thy	Tue Jul 14 10:53:44 2009 +0200
    12.2 +++ b/src/HOL/Library/Executable_Set.thy	Tue Jul 14 10:54:04 2009 +0200
    12.3 @@ -15,7 +15,7 @@
    12.4  definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    12.5    "subset = op \<le>"
    12.6  
    12.7 -declare subset_def [symmetric, code unfold]
    12.8 +declare subset_def [symmetric, code_unfold]
    12.9  
   12.10  lemma [code]:
   12.11    "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   12.12 @@ -25,7 +25,7 @@
   12.13    [code del]: "eq_set = op ="
   12.14  
   12.15  (* FIXME allow for Stefan's code generator:
   12.16 -declare set_eq_subset[code unfold]
   12.17 +declare set_eq_subset[code_unfold]
   12.18  *)
   12.19  
   12.20  lemma [code]:
   12.21 @@ -40,7 +40,7 @@
   12.22  
   12.23  subsection {* Rewrites for primitive operations *}
   12.24  
   12.25 -declare List_Set.project_def [symmetric, code unfold]
   12.26 +declare List_Set.project_def [symmetric, code_unfold]
   12.27  
   12.28  
   12.29  subsection {* code generator setup *}
    13.1 --- a/src/HOL/Library/Float.thy	Tue Jul 14 10:53:44 2009 +0200
    13.2 +++ b/src/HOL/Library/Float.thy	Tue Jul 14 10:54:04 2009 +0200
    13.3 @@ -19,7 +19,7 @@
    13.4    "of_float (Float a b) = real a * pow2 b"
    13.5  
    13.6  defs (overloaded)
    13.7 -  real_of_float_def [code unfold]: "real == of_float"
    13.8 +  real_of_float_def [code_unfold]: "real == of_float"
    13.9  
   13.10  primrec mantissa :: "float \<Rightarrow> int" where
   13.11    "mantissa (Float a b) = a"
   13.12 @@ -42,7 +42,7 @@
   13.13  instance ..
   13.14  end
   13.15  
   13.16 -lemma number_of_float_Float [code inline, symmetric, code post]:
   13.17 +lemma number_of_float_Float [code_inline, symmetric, code_post]:
   13.18    "number_of k = Float (number_of k) 0"
   13.19    by (simp add: number_of_float_def number_of_is_id)
   13.20  
    14.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Jul 14 10:53:44 2009 +0200
    14.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Jul 14 10:54:04 2009 +0200
    14.3 @@ -93,10 +93,10 @@
    14.4  begin
    14.5  
    14.6  definition
    14.7 -  Zero_fract_def [code, code unfold]: "0 = Fract 0 1"
    14.8 +  Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
    14.9  
   14.10  definition
   14.11 -  One_fract_def [code, code unfold]: "1 = Fract 1 1"
   14.12 +  One_fract_def [code, code_unfold]: "1 = Fract 1 1"
   14.13  
   14.14  definition
   14.15    add_fract_def [code del]:
   14.16 @@ -196,14 +196,14 @@
   14.17  lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
   14.18    by (rule of_nat_fract [symmetric])
   14.19  
   14.20 -lemma fract_collapse [code post]:
   14.21 +lemma fract_collapse [code_post]:
   14.22    "Fract 0 k = 0"
   14.23    "Fract 1 1 = 1"
   14.24    "Fract k 0 = 0"
   14.25    by (cases "k = 0")
   14.26      (simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def)
   14.27  
   14.28 -lemma fract_expand [code unfold]:
   14.29 +lemma fract_expand [code_unfold]:
   14.30    "0 = Fract 0 1"
   14.31    "1 = Fract 1 1"
   14.32    by (simp_all add: fract_collapse)
    15.1 --- a/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 10:53:44 2009 +0200
    15.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 10:54:04 2009 +0200
    15.3 @@ -40,10 +40,10 @@
    15.4    "0 = Fin 0"
    15.5  
    15.6  definition
    15.7 -  [code inline]: "1 = Fin 1"
    15.8 +  [code_inline]: "1 = Fin 1"
    15.9  
   15.10  definition
   15.11 -  [code inline, code del]: "number_of k = Fin (number_of k)"
   15.12 +  [code_inline, code del]: "number_of k = Fin (number_of k)"
   15.13  
   15.14  instance ..
   15.15  
    16.1 --- a/src/HOL/Library/Polynomial.thy	Tue Jul 14 10:53:44 2009 +0200
    16.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Jul 14 10:54:04 2009 +0200
    16.3 @@ -1505,7 +1505,7 @@
    16.4  
    16.5  code_datatype "0::'a::zero poly" pCons
    16.6  
    16.7 -declare pCons_0_0 [code post]
    16.8 +declare pCons_0_0 [code_post]
    16.9  
   16.10  instantiation poly :: ("{zero,eq}") eq
   16.11  begin
    17.1 --- a/src/HOL/List.thy	Tue Jul 14 10:53:44 2009 +0200
    17.2 +++ b/src/HOL/List.thy	Tue Jul 14 10:54:04 2009 +0200
    17.3 @@ -2076,7 +2076,7 @@
    17.4  by(induct xs) simp_all
    17.5  
    17.6  text{* For efficient code generation: avoid intermediate list. *}
    17.7 -lemma foldl_map[code unfold]:
    17.8 +lemma foldl_map[code_unfold]:
    17.9    "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
   17.10  by(induct xs arbitrary:a) simp_all
   17.11  
   17.12 @@ -2198,7 +2198,7 @@
   17.13  
   17.14  text{* For efficient code generation ---
   17.15         @{const listsum} is not tail recursive but @{const foldl} is. *}
   17.16 -lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
   17.17 +lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
   17.18  by(simp add:listsum_foldr foldl_foldr1)
   17.19  
   17.20  lemma distinct_listsum_conv_Setsum:
   17.21 @@ -3746,32 +3746,32 @@
   17.22    show ?case by (induct xs) (auto simp add: Cons aux)
   17.23  qed
   17.24  
   17.25 -lemma mem_iff [code post]:
   17.26 +lemma mem_iff [code_post]:
   17.27    "x mem xs \<longleftrightarrow> x \<in> set xs"
   17.28  by (induct xs) auto
   17.29  
   17.30 -lemmas in_set_code [code unfold] = mem_iff [symmetric]
   17.31 +lemmas in_set_code [code_unfold] = mem_iff [symmetric]
   17.32  
   17.33  lemma empty_null:
   17.34    "xs = [] \<longleftrightarrow> null xs"
   17.35  by (cases xs) simp_all
   17.36  
   17.37 -lemma [code inline]:
   17.38 +lemma [code_inline]:
   17.39    "eq_class.eq xs [] \<longleftrightarrow> null xs"
   17.40  by (simp add: eq empty_null)
   17.41  
   17.42 -lemmas null_empty [code post] =
   17.43 +lemmas null_empty [code_post] =
   17.44    empty_null [symmetric]
   17.45  
   17.46  lemma list_inter_conv:
   17.47    "set (list_inter xs ys) = set xs \<inter> set ys"
   17.48  by (induct xs) auto
   17.49  
   17.50 -lemma list_all_iff [code post]:
   17.51 +lemma list_all_iff [code_post]:
   17.52    "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
   17.53  by (induct xs) auto
   17.54  
   17.55 -lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
   17.56 +lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
   17.57  
   17.58  lemma list_all_append [simp]:
   17.59    "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
   17.60 @@ -3785,11 +3785,11 @@
   17.61    "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
   17.62    unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
   17.63  
   17.64 -lemma list_ex_iff [code post]:
   17.65 +lemma list_ex_iff [code_post]:
   17.66    "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
   17.67  by (induct xs) simp_all
   17.68  
   17.69 -lemmas list_bex_code [code unfold] =
   17.70 +lemmas list_bex_code [code_unfold] =
   17.71    list_ex_iff [symmetric]
   17.72  
   17.73  lemma list_ex_length:
   17.74 @@ -3804,7 +3804,7 @@
   17.75    "map_filter f P xs = map f (filter P xs)"
   17.76  by (induct xs) auto
   17.77  
   17.78 -lemma length_remdups_length_unique [code inline]:
   17.79 +lemma length_remdups_length_unique [code_inline]:
   17.80    "length (remdups xs) = length_unique xs"
   17.81    by (induct xs) simp_all
   17.82  
   17.83 @@ -3813,43 +3813,43 @@
   17.84  
   17.85  text {* Code for bounded quantification and summation over nats. *}
   17.86  
   17.87 -lemma atMost_upto [code unfold]:
   17.88 +lemma atMost_upto [code_unfold]:
   17.89    "{..n} = set [0..<Suc n]"
   17.90  by auto
   17.91  
   17.92 -lemma atLeast_upt [code unfold]:
   17.93 +lemma atLeast_upt [code_unfold]:
   17.94    "{..<n} = set [0..<n]"
   17.95  by auto
   17.96  
   17.97 -lemma greaterThanLessThan_upt [code unfold]:
   17.98 +lemma greaterThanLessThan_upt [code_unfold]:
   17.99    "{n<..<m} = set [Suc n..<m]"
  17.100  by auto
  17.101  
  17.102 -lemma atLeastLessThan_upt [code unfold]:
  17.103 +lemma atLeastLessThan_upt [code_unfold]:
  17.104    "{n..<m} = set [n..<m]"
  17.105  by auto
  17.106  
  17.107 -lemma greaterThanAtMost_upt [code unfold]:
  17.108 +lemma greaterThanAtMost_upt [code_unfold]:
  17.109    "{n<..m} = set [Suc n..<Suc m]"
  17.110  by auto
  17.111  
  17.112 -lemma atLeastAtMost_upt [code unfold]:
  17.113 +lemma atLeastAtMost_upt [code_unfold]:
  17.114    "{n..m} = set [n..<Suc m]"
  17.115  by auto
  17.116  
  17.117 -lemma all_nat_less_eq [code unfold]:
  17.118 +lemma all_nat_less_eq [code_unfold]:
  17.119    "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
  17.120  by auto
  17.121  
  17.122 -lemma ex_nat_less_eq [code unfold]:
  17.123 +lemma ex_nat_less_eq [code_unfold]:
  17.124    "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
  17.125  by auto
  17.126  
  17.127 -lemma all_nat_less [code unfold]:
  17.128 +lemma all_nat_less [code_unfold]:
  17.129    "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
  17.130  by auto
  17.131  
  17.132 -lemma ex_nat_less [code unfold]:
  17.133 +lemma ex_nat_less [code_unfold]:
  17.134    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
  17.135  by auto
  17.136  
  17.137 @@ -3857,30 +3857,30 @@
  17.138    "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
  17.139  by (induct xs) simp_all
  17.140  
  17.141 -lemma setsum_set_upt_conv_listsum [code unfold]:
  17.142 +lemma setsum_set_upt_conv_listsum [code_unfold]:
  17.143    "setsum f (set [m..<n]) = listsum (map f [m..<n])"
  17.144  by (rule setsum_set_distinct_conv_listsum) simp
  17.145  
  17.146  
  17.147  text {* Code for summation over ints. *}
  17.148  
  17.149 -lemma greaterThanLessThan_upto [code unfold]:
  17.150 +lemma greaterThanLessThan_upto [code_unfold]:
  17.151    "{i<..<j::int} = set [i+1..j - 1]"
  17.152  by auto
  17.153  
  17.154 -lemma atLeastLessThan_upto [code unfold]:
  17.155 +lemma atLeastLessThan_upto [code_unfold]:
  17.156    "{i..<j::int} = set [i..j - 1]"
  17.157  by auto
  17.158  
  17.159 -lemma greaterThanAtMost_upto [code unfold]:
  17.160 +lemma greaterThanAtMost_upto [code_unfold]:
  17.161    "{i<..j::int} = set [i+1..j]"
  17.162  by auto
  17.163  
  17.164 -lemma atLeastAtMost_upto [code unfold]:
  17.165 +lemma atLeastAtMost_upto [code_unfold]:
  17.166    "{i..j::int} = set [i..j]"
  17.167  by auto
  17.168  
  17.169 -lemma setsum_set_upto_conv_listsum [code unfold]:
  17.170 +lemma setsum_set_upto_conv_listsum [code_unfold]:
  17.171    "setsum f (set [i..j::int]) = listsum (map f [i..j])"
  17.172  by (rule setsum_set_distinct_conv_listsum) simp
  17.173  
    18.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Jul 14 10:53:44 2009 +0200
    18.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Jul 14 10:54:04 2009 +0200
    18.3 @@ -467,7 +467,7 @@
    18.4  
    18.5  lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
    18.6  
    18.7 -lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
    18.8 +lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
    18.9  
   18.10  code_module BV
   18.11  contains
    19.1 --- a/src/HOL/Nat.thy	Tue Jul 14 10:53:44 2009 +0200
    19.2 +++ b/src/HOL/Nat.thy	Tue Jul 14 10:54:04 2009 +0200
    19.3 @@ -1200,9 +1200,9 @@
    19.4  text {* for code generation *}
    19.5  
    19.6  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    19.7 -  funpow_code_def [code post]: "funpow = compow"
    19.8 +  funpow_code_def [code_post]: "funpow = compow"
    19.9  
   19.10 -lemmas [code unfold] = funpow_code_def [symmetric]
   19.11 +lemmas [code_unfold] = funpow_code_def [symmetric]
   19.12  
   19.13  lemma [code]:
   19.14    "funpow 0 f = id"
   19.15 @@ -1265,7 +1265,7 @@
   19.16  
   19.17  end
   19.18  
   19.19 -declare of_nat_code [code, code unfold, code inline del]
   19.20 +declare of_nat_code [code, code_unfold, code_inline del]
   19.21  
   19.22  text{*Class for unital semirings with characteristic zero.
   19.23   Includes non-ordered rings like the complex numbers.*}
    20.1 --- a/src/HOL/Nat_Numeral.thy	Tue Jul 14 10:53:44 2009 +0200
    20.2 +++ b/src/HOL/Nat_Numeral.thy	Tue Jul 14 10:54:04 2009 +0200
    20.3 @@ -20,13 +20,13 @@
    20.4  begin
    20.5  
    20.6  definition
    20.7 -  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
    20.8 +  nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
    20.9  
   20.10  instance ..
   20.11  
   20.12  end
   20.13  
   20.14 -lemma [code post]:
   20.15 +lemma [code_post]:
   20.16    "nat (number_of v) = number_of v"
   20.17    unfolding nat_number_of_def ..
   20.18  
   20.19 @@ -316,13 +316,13 @@
   20.20  lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
   20.21  by (simp add: nat_number_of_def)
   20.22  
   20.23 -lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
   20.24 +lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
   20.25  by (simp add: nat_number_of_def)
   20.26  
   20.27  lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
   20.28  by (simp add: nat_1 nat_number_of_def)
   20.29  
   20.30 -lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
   20.31 +lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
   20.32  by (simp add: nat_numeral_1_eq_1)
   20.33  
   20.34  
    21.1 --- a/src/HOL/Option.thy	Tue Jul 14 10:53:44 2009 +0200
    21.2 +++ b/src/HOL/Option.thy	Tue Jul 14 10:54:04 2009 +0200
    21.3 @@ -94,7 +94,7 @@
    21.4  subsubsection {* Code generator setup *}
    21.5  
    21.6  definition is_none :: "'a option \<Rightarrow> bool" where
    21.7 -  [code post]: "is_none x \<longleftrightarrow> x = None"
    21.8 +  [code_post]: "is_none x \<longleftrightarrow> x = None"
    21.9  
   21.10  lemma is_none_code [code]:
   21.11    shows "is_none None \<longleftrightarrow> True"
   21.12 @@ -105,7 +105,7 @@
   21.13    "is_none x \<longleftrightarrow> x = None"
   21.14    by (simp add: is_none_def)
   21.15  
   21.16 -lemma [code inline]:
   21.17 +lemma [code_inline]:
   21.18    "eq_class.eq x None \<longleftrightarrow> is_none x"
   21.19    by (simp add: eq is_none_none)
   21.20  
    22.1 --- a/src/HOL/Orderings.thy	Tue Jul 14 10:53:44 2009 +0200
    22.2 +++ b/src/HOL/Orderings.thy	Tue Jul 14 10:54:04 2009 +0200
    22.3 @@ -268,13 +268,13 @@
    22.4  
    22.5  text {* Explicit dictionaries for code generation *}
    22.6  
    22.7 -lemma min_ord_min [code, code unfold, code inline del]:
    22.8 +lemma min_ord_min [code, code_unfold, code_inline del]:
    22.9    "min = ord.min (op \<le>)"
   22.10    by (rule ext)+ (simp add: min_def ord.min_def)
   22.11  
   22.12  declare ord.min_def [code]
   22.13  
   22.14 -lemma max_ord_max [code, code unfold, code inline del]:
   22.15 +lemma max_ord_max [code, code_unfold, code_inline del]:
   22.16    "max = ord.max (op \<le>)"
   22.17    by (rule ext)+ (simp add: max_def ord.max_def)
   22.18  
    23.1 --- a/src/HOL/Power.thy	Tue Jul 14 10:53:44 2009 +0200
    23.2 +++ b/src/HOL/Power.thy	Tue Jul 14 10:54:04 2009 +0200
    23.3 @@ -455,7 +455,7 @@
    23.4  
    23.5  subsection {* Code generator tweak *}
    23.6  
    23.7 -lemma power_power_power [code, code unfold, code inline del]:
    23.8 +lemma power_power_power [code, code_unfold, code_inline del]:
    23.9    "power = power.power (1::'a::{power}) (op *)"
   23.10    unfolding power_def power.power_def ..
   23.11  
    24.1 --- a/src/HOL/Rational.thy	Tue Jul 14 10:53:44 2009 +0200
    24.2 +++ b/src/HOL/Rational.thy	Tue Jul 14 10:54:04 2009 +0200
    24.3 @@ -93,10 +93,10 @@
    24.4  begin
    24.5  
    24.6  definition
    24.7 -  Zero_rat_def [code, code unfold]: "0 = Fract 0 1"
    24.8 +  Zero_rat_def [code, code_unfold]: "0 = Fract 0 1"
    24.9  
   24.10  definition
   24.11 -  One_rat_def [code, code unfold]: "1 = Fract 1 1"
   24.12 +  One_rat_def [code, code_unfold]: "1 = Fract 1 1"
   24.13  
   24.14  definition
   24.15    add_rat_def [code del]:
   24.16 @@ -211,7 +211,7 @@
   24.17  
   24.18  end
   24.19  
   24.20 -lemma rat_number_collapse [code post]:
   24.21 +lemma rat_number_collapse [code_post]:
   24.22    "Fract 0 k = 0"
   24.23    "Fract 1 1 = 1"
   24.24    "Fract (number_of k) 1 = number_of k"
   24.25 @@ -219,7 +219,7 @@
   24.26    by (cases "k = 0")
   24.27      (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
   24.28  
   24.29 -lemma rat_number_expand [code unfold]:
   24.30 +lemma rat_number_expand [code_unfold]:
   24.31    "0 = Fract 0 1"
   24.32    "1 = Fract 1 1"
   24.33    "number_of k = Fract (number_of k) 1"
   24.34 @@ -291,11 +291,11 @@
   24.35  lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
   24.36    by (simp add: Fract_of_int_eq [symmetric])
   24.37  
   24.38 -lemma Fract_number_of_quotient [code post]:
   24.39 +lemma Fract_number_of_quotient [code_post]:
   24.40    "Fract (number_of k) (number_of l) = number_of k / number_of l"
   24.41    unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
   24.42  
   24.43 -lemma Fract_1_number_of [code post]:
   24.44 +lemma Fract_1_number_of [code_post]:
   24.45    "Fract 1 (number_of k) = 1 / number_of k"
   24.46    unfolding Fract_of_int_quotient number_of_eq by simp
   24.47  
   24.48 @@ -1003,7 +1003,7 @@
   24.49  
   24.50  definition (in term_syntax)
   24.51    valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
   24.52 -  [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
   24.53 +  [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
   24.54  
   24.55  notation fcomp (infixl "o>" 60)
   24.56  notation scomp (infixl "o\<rightarrow>" 60)
    25.1 --- a/src/HOL/RealDef.thy	Tue Jul 14 10:53:44 2009 +0200
    25.2 +++ b/src/HOL/RealDef.thy	Tue Jul 14 10:54:04 2009 +0200
    25.3 @@ -559,8 +559,8 @@
    25.4    real :: "'a => real"
    25.5  
    25.6  defs (overloaded)
    25.7 -  real_of_nat_def [code unfold]: "real == real_of_nat"
    25.8 -  real_of_int_def [code unfold]: "real == real_of_int"
    25.9 +  real_of_nat_def [code_unfold]: "real == real_of_nat"
   25.10 +  real_of_int_def [code_unfold]: "real == real_of_int"
   25.11  
   25.12  lemma real_eq_of_nat: "real = of_nat"
   25.13    unfolding real_of_nat_def ..
   25.14 @@ -946,7 +946,7 @@
   25.15  
   25.16  end
   25.17  
   25.18 -lemma [code unfold, symmetric, code post]:
   25.19 +lemma [code_unfold, symmetric, code_post]:
   25.20    "number_of k = real_of_int (number_of k)"
   25.21    unfolding number_of_is_id real_number_of_def ..
   25.22  
   25.23 @@ -1061,29 +1061,29 @@
   25.24  
   25.25  code_datatype Ratreal
   25.26  
   25.27 -lemma Ratreal_number_collapse [code post]:
   25.28 +lemma Ratreal_number_collapse [code_post]:
   25.29    "Ratreal 0 = 0"
   25.30    "Ratreal 1 = 1"
   25.31    "Ratreal (number_of k) = number_of k"
   25.32  by simp_all
   25.33  
   25.34 -lemma zero_real_code [code, code unfold]:
   25.35 +lemma zero_real_code [code, code_unfold]:
   25.36    "0 = Ratreal 0"
   25.37  by simp
   25.38  
   25.39 -lemma one_real_code [code, code unfold]:
   25.40 +lemma one_real_code [code, code_unfold]:
   25.41    "1 = Ratreal 1"
   25.42  by simp
   25.43  
   25.44 -lemma number_of_real_code [code unfold]:
   25.45 +lemma number_of_real_code [code_unfold]:
   25.46    "number_of k = Ratreal (number_of k)"
   25.47  by simp
   25.48  
   25.49 -lemma Ratreal_number_of_quotient [code post]:
   25.50 +lemma Ratreal_number_of_quotient [code_post]:
   25.51    "Ratreal (number_of r) / Ratreal (number_of s) = number_of r / number_of s"
   25.52  by simp
   25.53  
   25.54 -lemma Ratreal_number_of_quotient2 [code post]:
   25.55 +lemma Ratreal_number_of_quotient2 [code_post]:
   25.56    "Ratreal (number_of r / number_of s) = number_of r / number_of s"
   25.57  unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
   25.58  
   25.59 @@ -1129,7 +1129,7 @@
   25.60  
   25.61  definition (in term_syntax)
   25.62    valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
   25.63 -  [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
   25.64 +  [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
   25.65  
   25.66  notation fcomp (infixl "o>" 60)
   25.67  notation scomp (infixl "o\<rightarrow>" 60)
    26.1 --- a/src/HOL/SetInterval.thy	Tue Jul 14 10:53:44 2009 +0200
    26.2 +++ b/src/HOL/SetInterval.thy	Tue Jul 14 10:54:04 2009 +0200
    26.3 @@ -284,8 +284,8 @@
    26.4  lemma atLeast0AtMost: "{0..n::nat} = {..n}"
    26.5  by(simp add:atMost_def atLeastAtMost_def)
    26.6  
    26.7 -declare atLeast0LessThan[symmetric, code unfold]
    26.8 -        atLeast0AtMost[symmetric, code unfold]
    26.9 +declare atLeast0LessThan[symmetric, code_unfold]
   26.10 +        atLeast0AtMost[symmetric, code_unfold]
   26.11  
   26.12  lemma atLeastLessThan0: "{m..<0::nat} = {}"
   26.13  by (simp add: atLeastLessThan_def)
    27.1 --- a/src/HOL/String.thy	Tue Jul 14 10:53:44 2009 +0200
    27.2 +++ b/src/HOL/String.thy	Tue Jul 14 10:54:04 2009 +0200
    27.3 @@ -58,11 +58,11 @@
    27.4  end
    27.5  *}
    27.6  
    27.7 -lemma char_case_nibble_pair [code, code inline]:
    27.8 +lemma char_case_nibble_pair [code, code_inline]:
    27.9    "char_case f = split f o nibble_pair_of_char"
   27.10    by (simp add: expand_fun_eq split: char.split)
   27.11  
   27.12 -lemma char_rec_nibble_pair [code, code inline]:
   27.13 +lemma char_rec_nibble_pair [code, code_inline]:
   27.14    "char_rec f = split f o nibble_pair_of_char"
   27.15    unfolding char_case_nibble_pair [symmetric]
   27.16    by (simp add: expand_fun_eq split: char.split)
    28.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Jul 14 10:53:44 2009 +0200
    28.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jul 14 10:54:04 2009 +0200
    28.3 @@ -697,7 +697,8 @@
    28.4  
    28.5  val setup =
    28.6    add_codegen "inductive" inductive_codegen #>
    28.7 -  Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
    28.8 -    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
    28.9 +  Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
   28.10 +    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
   28.11 +    "introduction rules for executable predicates";
   28.12  
   28.13  end;
    29.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Jul 14 10:53:44 2009 +0200
    29.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Jul 14 10:54:04 2009 +0200
    29.3 @@ -541,8 +541,9 @@
    29.4      "declare rules for converting between predicate and set notation" #>
    29.5    Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
    29.6    Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
    29.7 -  Code.add_attribute ("ind_set",
    29.8 -    Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
    29.9 +  Attrib.setup @{binding code_ind_set}
   29.10 +    (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
   29.11 +    "introduction rules for executable predicates" #>
   29.12    Codegen.add_preprocessor codegen_preproc #>
   29.13    Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
   29.14      "declaration of monotonicity rule for set operators" #>
    30.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Jul 14 10:53:44 2009 +0200
    30.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jul 14 10:54:04 2009 +0200
    30.3 @@ -23,15 +23,13 @@
    30.4    fun merge _ = Symtab.merge (K true);
    30.5  );
    30.6  
    30.7 -fun add_thm NONE thm thy = Code.add_eqn thm thy
    30.8 -  | add_thm (SOME module_name) thm thy =
    30.9 -      let
   30.10 -        val (thm', _) = Code.mk_eqn thy (thm, true)
   30.11 -      in
   30.12 -        thy
   30.13 -        |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
   30.14 -        |> Code.add_eqn thm'
   30.15 -      end;
   30.16 +fun add_thm_target module_name thm thy =
   30.17 +  let
   30.18 +    val (thm', _) = Code.mk_eqn thy (thm, true)
   30.19 +  in
   30.20 +    thy
   30.21 +    |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
   30.22 +  end;
   30.23  
   30.24  fun expand_eta thy [] = []
   30.25    | expand_eta thy (thms as thm :: _) =
   30.26 @@ -163,15 +161,8 @@
   30.27          end)
   30.28    | _ => NONE);
   30.29  
   30.30 -val setup = let
   30.31 -  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
   30.32 -    (add_thm opt_module thm) I);
   30.33 -  val del = Thm.declaration_attribute (fn thm => Context.mapping
   30.34 -    (Code.del_eqn thm) I);
   30.35 -in
   30.36 +val setup = 
   30.37    add_codegen "recfun" recfun_codegen
   30.38 -  #> Code.add_attribute ("", Args.del |-- Scan.succeed del
   30.39 -     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
   30.40 -end;
   30.41 +  #> Code.set_code_target_attr add_thm_target;
   30.42  
   30.43  end;
    31.1 --- a/src/HOL/ex/Numeral.thy	Tue Jul 14 10:53:44 2009 +0200
    31.2 +++ b/src/HOL/ex/Numeral.thy	Tue Jul 14 10:54:04 2009 +0200
    31.3 @@ -751,14 +751,14 @@
    31.4  subsection {* Code generator setup for @{typ int} *}
    31.5  
    31.6  definition Pls :: "num \<Rightarrow> int" where
    31.7 -  [simp, code post]: "Pls n = of_num n"
    31.8 +  [simp, code_post]: "Pls n = of_num n"
    31.9  
   31.10  definition Mns :: "num \<Rightarrow> int" where
   31.11 -  [simp, code post]: "Mns n = - of_num n"
   31.12 +  [simp, code_post]: "Mns n = - of_num n"
   31.13  
   31.14  code_datatype "0::int" Pls Mns
   31.15  
   31.16 -lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
   31.17 +lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
   31.18  
   31.19  definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   31.20    [simp, code del]: "sub m n = (of_num m - of_num n)"
   31.21 @@ -874,10 +874,10 @@
   31.22    using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   31.23    by (simp_all add: of_num_less_iff)
   31.24  
   31.25 -lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp
   31.26 -lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp
   31.27 -declare zero_is_num_zero [code inline del]
   31.28 -declare one_is_num_one [code inline del]
   31.29 +lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
   31.30 +lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
   31.31 +declare zero_is_num_zero [code_inline del]
   31.32 +declare one_is_num_one [code_inline del]
   31.33  
   31.34  hide (open) const sub dup
   31.35  
    32.1 --- a/src/Pure/Isar/code.ML	Tue Jul 14 10:53:44 2009 +0200
    32.2 +++ b/src/Pure/Isar/code.ML	Tue Jul 14 10:54:04 2009 +0200
    32.3 @@ -62,7 +62,7 @@
    32.4    val print_codesetup: theory -> unit
    32.5  
    32.6    (*infrastructure*)
    32.7 -  val add_attribute: string * attribute parser -> theory -> theory
    32.8 +  val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
    32.9    val purge_data: theory -> theory
   32.10  end;
   32.11  
   32.12 @@ -235,31 +235,6 @@
   32.13    end;
   32.14  
   32.15  
   32.16 -(** code attributes **)
   32.17 -
   32.18 -structure Code_Attr = TheoryDataFun (
   32.19 -  type T = (string * attribute parser) list;
   32.20 -  val empty = [];
   32.21 -  val copy = I;
   32.22 -  val extend = I;
   32.23 -  fun merge _ = AList.merge (op = : string * string -> bool) (K true);
   32.24 -);
   32.25 -
   32.26 -fun add_attribute (attr as (name, _)) =
   32.27 -  let
   32.28 -    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
   32.29 -      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
   32.30 -  in Code_Attr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
   32.31 -    then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
   32.32 -  end;
   32.33 -
   32.34 -val _ = Context.>> (Context.map_theory
   32.35 -  (Attrib.setup (Binding.name "code")
   32.36 -    (Scan.peek (fn context =>
   32.37 -      List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context)))))
   32.38 -    "declare theorems for code generation"));
   32.39 -
   32.40 -
   32.41  (** data store **)
   32.42  
   32.43  (* code equations *)
   32.44 @@ -543,7 +518,7 @@
   32.45        in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
   32.46      fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
   32.47        let
   32.48 -        val _ = if tyco' <> tyco
   32.49 +        val _ = if (tyco' : string) <> tyco
   32.50            then error "Different type constructors in constructor set"
   32.51            else ();
   32.52          val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
   32.53 @@ -911,18 +886,32 @@
   32.54   of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   32.55    | NONE => thy;
   32.56  
   32.57 +structure Code_Attr = TheoryDataFun (
   32.58 +  type T = (string -> thm -> theory -> theory) option;
   32.59 +  val empty = NONE;
   32.60 +  val copy = I;
   32.61 +  val extend = I;
   32.62 +  fun merge _ (NONE, f2) = f2
   32.63 +    | merge _ (f1, _) = f1;
   32.64 +);
   32.65 +
   32.66 +fun set_code_target_attr f = Code_Attr.map (K (SOME f));
   32.67 +
   32.68  val _ = Context.>> (Context.map_theory
   32.69    (let
   32.70      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   32.71 -    fun add_simple_attribute (name, f) =
   32.72 -      add_attribute (name, Scan.succeed (mk_attribute f));
   32.73 -    fun add_del_attribute (name, (add, del)) =
   32.74 -      add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
   32.75 -        || Scan.succeed (mk_attribute add))
   32.76 +    val code_attribute_parser =
   32.77 +      Args.del |-- Scan.succeed (mk_attribute del_eqn)
   32.78 +      || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
   32.79 +      || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
   32.80 +           (fn prefix => mk_attribute (fn thm => fn thy => thy
   32.81 +             |> add_warning_eqn thm
   32.82 +             |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
   32.83 +      || Scan.succeed (mk_attribute add_warning_eqn);
   32.84    in
   32.85      Type_Interpretation.init
   32.86 -    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
   32.87 -    #> add_simple_attribute ("nbe", add_nbe_eqn)
   32.88 +    #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
   32.89 +        "declare theorems for code generation"
   32.90    end));
   32.91  
   32.92  
    33.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jul 14 10:53:44 2009 +0200
    33.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jul 14 10:54:04 2009 +0200
    33.3 @@ -526,14 +526,16 @@
    33.4  val setup = 
    33.5    let
    33.6      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    33.7 -    fun add_del_attribute (name, (add, del)) =
    33.8 -      Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
    33.9 -        || Scan.succeed (mk_attribute add))
   33.10 +    fun add_del_attribute_parser (add, del) =
   33.11 +      Attrib.add_del (mk_attribute add) (mk_attribute del);
   33.12    in
   33.13 -    add_del_attribute ("inline", (add_inline, del_inline))
   33.14 -    #> add_del_attribute ("post", (add_post, del_post))
   33.15 -    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
   33.16 -       (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I)))
   33.17 +    Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
   33.18 +        "preprocessing equations for code generator"
   33.19 +    #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
   33.20 +        "postprocessing equations for code generator"
   33.21 +    #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
   33.22 +       (fn thm => Codegen.add_unfold thm #> add_inline thm)))
   33.23 +        "preprocessing equations for code generators"
   33.24    end;
   33.25  
   33.26  val _ =