avoid local [code]
authorhaftmann
Thu Apr 23 12:17:50 2009 +0200 (2009-04-23)
changeset 3096655104c664185
parent 30965 e0938d929bfd
child 30967 b5d67f83576e
avoid local [code]
src/HOL/HOL.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 22 19:16:02 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Apr 23 12:17:50 2009 +0200
     1.3 @@ -1737,13 +1737,16 @@
     1.4  lemma eq_refl: "eq x x \<longleftrightarrow> True"
     1.5    unfolding eq by rule+
     1.6  
     1.7 -lemma equals_eq [code inline, code]: "(op =) \<equiv> eq"
     1.8 +lemma equals_eq [code inline]: "(op =) \<equiv> eq"
     1.9    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    1.10  
    1.11  declare equals_eq [symmetric, code post]
    1.12  
    1.13  end
    1.14  
    1.15 +declare equals_eq [code]
    1.16 +
    1.17 +
    1.18  subsubsection {* Generic code generator foundation *}
    1.19  
    1.20  text {* Datatypes *}
     2.1 --- a/src/HOL/Nat.thy	Wed Apr 22 19:16:02 2009 +0200
     2.2 +++ b/src/HOL/Nat.thy	Thu Apr 23 12:17:50 2009 +0200
     2.3 @@ -1220,7 +1220,7 @@
     2.4    "of_nat_aux inc 0 i = i"
     2.5    | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
     2.6  
     2.7 -lemma of_nat_code [code, code unfold, code inline del]:
     2.8 +lemma of_nat_code:
     2.9    "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
    2.10  proof (induct n)
    2.11    case 0 then show ?case by simp
    2.12 @@ -1232,9 +1232,11 @@
    2.13      by simp
    2.14    with Suc show ?case by (simp add: add_commute)
    2.15  qed
    2.16 -    
    2.17 +
    2.18  end
    2.19  
    2.20 +declare of_nat_code [code, code unfold, code inline del]
    2.21 +
    2.22  text{*Class for unital semirings with characteristic zero.
    2.23   Includes non-ordered rings like the complex numbers.*}
    2.24