dropped superfluous [code del]s
authorhaftmann
Mon Jul 12 08:58:13 2010 +0200 (2010-07-12)
changeset 3776526bdfb7b680b
parent 37764 3489daf839d5
child 37766 a779f463bae4
dropped superfluous [code del]s
src/HOL/Archimedean_Field.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Enum.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Fset.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Matrix/Matrix.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/Number_Theory/Primes.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Product_Type.thy
src/HOL/RealDef.thy
src/HOL/SupInf.thy
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/Gauge_Integration.thy
src/HOL/ex/Numeral.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4  
     1.5  definition
     1.6    floor :: "'a::archimedean_field \<Rightarrow> int" where
     1.7 -  [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
     1.8 +  "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
     1.9  
    1.10  notation (xsymbols)
    1.11    floor  ("\<lfloor>_\<rfloor>")
    1.12 @@ -274,7 +274,7 @@
    1.13  
    1.14  definition
    1.15    ceiling :: "'a::archimedean_field \<Rightarrow> int" where
    1.16 -  [code del]: "ceiling x = - floor (- x)"
    1.17 +  "ceiling x = - floor (- x)"
    1.18  
    1.19  notation (xsymbols)
    1.20    ceiling  ("\<lceil>_\<rceil>")
     2.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Jul 12 08:58:12 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Jul 12 08:58:13 2010 +0200
     2.3 @@ -42,7 +42,7 @@
     2.4  definition
     2.5    traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
     2.6  where
     2.7 -[code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
     2.8 +  "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
     2.9                                  | Node x r \<Rightarrow> (do tl \<leftarrow> Ref.lookup r;
    2.10                                                    return (Inr tl) done))
    2.11                     (\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
     3.1 --- a/src/HOL/Library/Char_ord.thy	Mon Jul 12 08:58:12 2010 +0200
     3.2 +++ b/src/HOL/Library/Char_ord.thy	Mon Jul 12 08:58:13 2010 +0200
     3.3 @@ -63,11 +63,11 @@
     3.4  begin
     3.5  
     3.6  definition
     3.7 -  char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
     3.8 +  char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
     3.9      n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
    3.10  
    3.11  definition
    3.12 -  char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    3.13 +  char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    3.14      n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
    3.15  
    3.16  instance
     4.1 --- a/src/HOL/Library/ContNotDenum.thy	Mon Jul 12 08:58:12 2010 +0200
     4.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Jul 12 08:58:13 2010 +0200
     4.3 @@ -402,7 +402,6 @@
     4.4         (f (Suc n)) \<notin> e)
     4.5        )"
     4.6  
     4.7 -declare newInt.simps [code del]
     4.8  
     4.9  subsubsection {* Properties *}
    4.10  
     5.1 --- a/src/HOL/Library/Dlist.thy	Mon Jul 12 08:58:12 2010 +0200
     5.2 +++ b/src/HOL/Library/Dlist.thy	Mon Jul 12 08:58:13 2010 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
     5.5  
     5.6  definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
     5.7 -  [code del]: "Dlist xs = Abs_dlist (remdups xs)"
     5.8 +  "Dlist xs = Abs_dlist (remdups xs)"
     5.9  
    5.10  lemma distinct_list_of_dlist [simp]:
    5.11    "distinct (list_of_dlist dxs)"
     6.1 --- a/src/HOL/Library/Enum.thy	Mon Jul 12 08:58:12 2010 +0200
     6.2 +++ b/src/HOL/Library/Enum.thy	Mon Jul 12 08:58:13 2010 +0200
     6.3 @@ -149,7 +149,7 @@
     6.4  begin
     6.5  
     6.6  definition
     6.7 -  [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)"
     6.8 +  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
     6.9  
    6.10  instance proof
    6.11    show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
    6.12 @@ -278,7 +278,7 @@
    6.13  begin
    6.14  
    6.15  definition
    6.16 -  [code del]: "enum = map (split Char) (product enum enum)"
    6.17 +  "enum = map (split Char) (product enum enum)"
    6.18  
    6.19  lemma enum_chars [code]:
    6.20    "enum = chars"
     7.1 --- a/src/HOL/Library/Fraction_Field.thy	Mon Jul 12 08:58:12 2010 +0200
     7.2 +++ b/src/HOL/Library/Fraction_Field.thy	Mon Jul 12 08:58:13 2010 +0200
     7.3 @@ -69,7 +69,7 @@
     7.4  
     7.5  definition
     7.6    Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
     7.7 -  [code del]: "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
     7.8 +  "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
     7.9  
    7.10  code_datatype Fract
    7.11  
    7.12 @@ -93,13 +93,13 @@
    7.13  begin
    7.14  
    7.15  definition
    7.16 -  Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
    7.17 +  Zero_fract_def [code_unfold]: "0 = Fract 0 1"
    7.18  
    7.19  definition
    7.20 -  One_fract_def [code, code_unfold]: "1 = Fract 1 1"
    7.21 +  One_fract_def [code_unfold]: "1 = Fract 1 1"
    7.22  
    7.23  definition
    7.24 -  add_fract_def [code del]:
    7.25 +  add_fract_def:
    7.26    "q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
    7.27      fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
    7.28  
    7.29 @@ -115,7 +115,7 @@
    7.30  qed
    7.31  
    7.32  definition
    7.33 -  minus_fract_def [code del]:
    7.34 +  minus_fract_def:
    7.35    "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})"
    7.36  
    7.37  lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
    7.38 @@ -129,7 +129,7 @@
    7.39    by (cases "b = 0") (simp_all add: eq_fract)
    7.40  
    7.41  definition
    7.42 -  diff_fract_def [code del]: "q - r = q + - (r::'a fract)"
    7.43 +  diff_fract_def: "q - r = q + - (r::'a fract)"
    7.44  
    7.45  lemma diff_fract [simp]:
    7.46    assumes "b \<noteq> 0" and "d \<noteq> 0"
    7.47 @@ -137,7 +137,7 @@
    7.48    using assms by (simp add: diff_fract_def diff_minus)
    7.49  
    7.50  definition
    7.51 -  mult_fract_def [code del]:
    7.52 +  mult_fract_def:
    7.53    "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
    7.54      fractrel``{(fst x * fst y, snd x * snd y)})"
    7.55  
    7.56 @@ -236,7 +236,7 @@
    7.57  begin
    7.58  
    7.59  definition
    7.60 -  inverse_fract_def [code del]:
    7.61 +  inverse_fract_def:
    7.62    "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.
    7.63       fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
    7.64  
    7.65 @@ -250,7 +250,7 @@
    7.66  qed
    7.67  
    7.68  definition
    7.69 -  divide_fract_def [code del]: "q / r = q * inverse (r:: 'a fract)"
    7.70 +  divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
    7.71  
    7.72  lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
    7.73    by (simp add: divide_fract_def)
    7.74 @@ -318,12 +318,12 @@
    7.75  begin
    7.76  
    7.77  definition
    7.78 -  le_fract_def [code del]:
    7.79 +  le_fract_def:
    7.80     "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
    7.81        {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
    7.82  
    7.83  definition
    7.84 -  less_fract_def [code del]: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
    7.85 +  less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
    7.86  
    7.87  lemma le_fract [simp]:
    7.88    assumes "b \<noteq> 0" and "d \<noteq> 0"
     8.1 --- a/src/HOL/Library/Fset.thy	Mon Jul 12 08:58:12 2010 +0200
     8.2 +++ b/src/HOL/Library/Fset.thy	Mon Jul 12 08:58:13 2010 +0200
     8.3 @@ -124,10 +124,10 @@
     8.4  begin
     8.5  
     8.6  definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where
     8.7 -  [simp, code del]: "Inf_fset As = Fset (Inf (image member As))"
     8.8 +  [simp]: "Inf_fset As = Fset (Inf (image member As))"
     8.9  
    8.10  definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where
    8.11 -  [simp, code del]: "Sup_fset As = Fset (Sup (image member As))"
    8.12 +  [simp]: "Sup_fset As = Fset (Sup (image member As))"
    8.13  
    8.14  instance proof
    8.15  qed (auto simp add: le_fun_def le_bool_def)
     9.1 --- a/src/HOL/Library/List_lexord.thy	Mon Jul 12 08:58:12 2010 +0200
     9.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Jul 12 08:58:13 2010 +0200
     9.3 @@ -62,10 +62,10 @@
     9.4  begin
     9.5  
     9.6  definition
     9.7 -  [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
     9.8 +  "(inf \<Colon> 'a list \<Rightarrow> _) = min"
     9.9  
    9.10  definition
    9.11 -  [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    9.12 +  "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    9.13  
    9.14  instance
    9.15    by intro_classes
    10.1 --- a/src/HOL/Library/Multiset.thy	Mon Jul 12 08:58:12 2010 +0200
    10.2 +++ b/src/HOL/Library/Multiset.thy	Mon Jul 12 08:58:13 2010 +0200
    10.3 @@ -978,11 +978,11 @@
    10.4  subsubsection {* Well-foundedness *}
    10.5  
    10.6  definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
    10.7 -  [code del]: "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
    10.8 +  "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
    10.9        (\<forall>b. b :# K --> (b, a) \<in> r)}"
   10.10  
   10.11  definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   10.12 -  [code del]: "mult r = (mult1 r)\<^sup>+"
   10.13 +  "mult r = (mult1 r)\<^sup>+"
   10.14  
   10.15  lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   10.16  by (simp add: mult1_def)
   10.17 @@ -1498,7 +1498,7 @@
   10.18    by auto
   10.19  
   10.20  definition "ms_strict = mult pair_less"
   10.21 -definition [code del]: "ms_weak = ms_strict \<union> Id"
   10.22 +definition "ms_weak = ms_strict \<union> Id"
   10.23  
   10.24  lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
   10.25  unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
    11.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Jul 12 08:58:12 2010 +0200
    11.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Jul 12 08:58:13 2010 +0200
    11.3 @@ -126,7 +126,7 @@
    11.4  begin
    11.5  
    11.6  definition
    11.7 -  [code del]: "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
    11.8 +  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
    11.9  
   11.10  lemma plus_inat_simps [simp, code]:
   11.11    "Fin m + Fin n = Fin (m + n)"
   11.12 @@ -177,7 +177,7 @@
   11.13  begin
   11.14  
   11.15  definition
   11.16 -  times_inat_def [code del]:
   11.17 +  times_inat_def:
   11.18    "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
   11.19      (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
   11.20  
   11.21 @@ -238,11 +238,11 @@
   11.22  begin
   11.23  
   11.24  definition
   11.25 -  [code del]: "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   11.26 +  "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   11.27      | \<infinity> \<Rightarrow> True)"
   11.28  
   11.29  definition
   11.30 -  [code del]: "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   11.31 +  "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   11.32      | \<infinity> \<Rightarrow> False)"
   11.33  
   11.34  lemma inat_ord_simps [simp]:
    12.1 --- a/src/HOL/Library/Option_ord.thy	Mon Jul 12 08:58:12 2010 +0200
    12.2 +++ b/src/HOL/Library/Option_ord.thy	Mon Jul 12 08:58:13 2010 +0200
    12.3 @@ -12,10 +12,10 @@
    12.4  begin
    12.5  
    12.6  definition less_eq_option where
    12.7 -  [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))"
    12.8 +  "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))"
    12.9  
   12.10  definition less_option where
   12.11 -  [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))"
   12.12 +  "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
   12.13  
   12.14  lemma less_eq_option_None [simp]: "None \<le> x"
   12.15    by (simp add: less_eq_option_def)
    13.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jul 12 08:58:12 2010 +0200
    13.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jul 12 08:58:13 2010 +0200
    13.3 @@ -98,7 +98,7 @@
    13.4  definition
    13.5    pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    13.6  where
    13.7 -  [code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"
    13.8 +  "pCons a p = Abs_poly (nat_case a (coeff p))"
    13.9  
   13.10  syntax
   13.11    "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
   13.12 @@ -209,7 +209,7 @@
   13.13  function
   13.14    poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"
   13.15  where
   13.16 -  poly_rec_pCons_eq_if [simp del, code del]:
   13.17 +  poly_rec_pCons_eq_if [simp del]:
   13.18      "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"
   13.19  by (case_tac x, rename_tac q, case_tac q, auto)
   13.20  
   13.21 @@ -266,7 +266,7 @@
   13.22  begin
   13.23  
   13.24  definition
   13.25 -  plus_poly_def [code del]:
   13.26 +  plus_poly_def:
   13.27      "p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"
   13.28  
   13.29  lemma Poly_add:
   13.30 @@ -305,11 +305,11 @@
   13.31  begin
   13.32  
   13.33  definition
   13.34 -  uminus_poly_def [code del]:
   13.35 +  uminus_poly_def:
   13.36      "- p = Abs_poly (\<lambda>n. - coeff p n)"
   13.37  
   13.38  definition
   13.39 -  minus_poly_def [code del]:
   13.40 +  minus_poly_def:
   13.41      "p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"
   13.42  
   13.43  lemma Poly_minus:
   13.44 @@ -512,7 +512,7 @@
   13.45  begin
   13.46  
   13.47  definition
   13.48 -  times_poly_def [code del]:
   13.49 +  times_poly_def:
   13.50      "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"
   13.51  
   13.52  lemma mult_poly_0_left: "(0::'a poly) * q = 0"
   13.53 @@ -736,20 +736,16 @@
   13.54  begin
   13.55  
   13.56  definition
   13.57 -  [code del]:
   13.58 -    "x < y \<longleftrightarrow> pos_poly (y - x)"
   13.59 +  "x < y \<longleftrightarrow> pos_poly (y - x)"
   13.60  
   13.61  definition
   13.62 -  [code del]:
   13.63 -    "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
   13.64 +  "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
   13.65  
   13.66  definition
   13.67 -  [code del]:
   13.68 -    "abs (x::'a poly) = (if x < 0 then - x else x)"
   13.69 +  "abs (x::'a poly) = (if x < 0 then - x else x)"
   13.70  
   13.71  definition
   13.72 -  [code del]:
   13.73 -    "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   13.74 +  "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   13.75  
   13.76  instance proof
   13.77    fix x y :: "'a poly"
   13.78 @@ -818,7 +814,6 @@
   13.79  definition
   13.80    pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
   13.81  where
   13.82 -  [code del]:
   13.83    "pdivmod_rel x y q r \<longleftrightarrow>
   13.84      x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
   13.85  
   13.86 @@ -943,10 +938,10 @@
   13.87  begin
   13.88  
   13.89  definition div_poly where
   13.90 -  [code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
   13.91 +  "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
   13.92  
   13.93  definition mod_poly where
   13.94 -  [code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
   13.95 +  "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
   13.96  
   13.97  lemma div_poly_eq:
   13.98    "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
   13.99 @@ -1133,7 +1128,7 @@
  13.100  by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
  13.101     (auto dest: degree_mod_less)
  13.102  
  13.103 -declare poly_gcd.simps [simp del, code del]
  13.104 +declare poly_gcd.simps [simp del]
  13.105  
  13.106  lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x"
  13.107    and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
  13.108 @@ -1287,7 +1282,7 @@
  13.109  
  13.110  definition
  13.111    synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
  13.112 -where [code del]:
  13.113 +where
  13.114    "synthetic_divmod p c =
  13.115      poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p"
  13.116  
  13.117 @@ -1442,7 +1437,6 @@
  13.118  definition
  13.119    order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
  13.120  where
  13.121 -  [code del]:
  13.122    "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
  13.123  
  13.124  lemma coeff_linear_power:
  13.125 @@ -1514,7 +1508,7 @@
  13.126  instantiation poly :: ("{zero,eq}") eq
  13.127  begin
  13.128  
  13.129 -definition [code del]:
  13.130 +definition
  13.131    "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
  13.132  
  13.133  instance
  13.134 @@ -1574,7 +1568,7 @@
  13.135  definition
  13.136    pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
  13.137  where
  13.138 -  [code del]: "pdivmod x y = (x div y, x mod y)"
  13.139 +  "pdivmod x y = (x div y, x mod y)"
  13.140  
  13.141  lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
  13.142    unfolding pdivmod_def by simp
    14.1 --- a/src/HOL/Library/Product_ord.thy	Mon Jul 12 08:58:12 2010 +0200
    14.2 +++ b/src/HOL/Library/Product_ord.thy	Mon Jul 12 08:58:13 2010 +0200
    14.3 @@ -12,10 +12,10 @@
    14.4  begin
    14.5  
    14.6  definition
    14.7 -  prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
    14.8 +  prod_le_def: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
    14.9  
   14.10  definition
   14.11 -  prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
   14.12 +  prod_less_def: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
   14.13  
   14.14  instance ..
   14.15  
    15.1 --- a/src/HOL/Library/Sublist_Order.thy	Mon Jul 12 08:58:12 2010 +0200
    15.2 +++ b/src/HOL/Library/Sublist_Order.thy	Mon Jul 12 08:58:13 2010 +0200
    15.3 @@ -26,7 +26,7 @@
    15.4    | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
    15.5  
    15.6  definition
    15.7 -  [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    15.8 +  "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    15.9  
   15.10  instance proof qed
   15.11  
    16.1 --- a/src/HOL/Library/Univ_Poly.thy	Mon Jul 12 08:58:12 2010 +0200
    16.2 +++ b/src/HOL/Library/Univ_Poly.thy	Mon Jul 12 08:58:13 2010 +0200
    16.3 @@ -71,7 +71,7 @@
    16.4  
    16.5  definition (in semiring_0)
    16.6    divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "divides" 70) where
    16.7 -  [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
    16.8 +  "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
    16.9  
   16.10      --{*order of a polynomial*}
   16.11  definition (in ring_1) order :: "'a => 'a list => nat" where
    17.1 --- a/src/HOL/Matrix/Matrix.thy	Mon Jul 12 08:58:12 2010 +0200
    17.2 +++ b/src/HOL/Matrix/Matrix.thy	Mon Jul 12 08:58:13 2010 +0200
    17.3 @@ -776,7 +776,7 @@
    17.4  instantiation matrix :: (zero) zero
    17.5  begin
    17.6  
    17.7 -definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
    17.8 +definition zero_matrix_def: "0 = Abs_matrix (\<lambda>j i. 0)"
    17.9  
   17.10  instance ..
   17.11  
   17.12 @@ -1459,9 +1459,9 @@
   17.13  instantiation matrix :: ("{lattice, zero}") lattice
   17.14  begin
   17.15  
   17.16 -definition [code del]: "inf = combine_matrix inf"
   17.17 +definition "inf = combine_matrix inf"
   17.18  
   17.19 -definition [code del]: "sup = combine_matrix sup"
   17.20 +definition "sup = combine_matrix sup"
   17.21  
   17.22  instance
   17.23    by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
   17.24 @@ -1472,7 +1472,7 @@
   17.25  begin
   17.26  
   17.27  definition
   17.28 -  plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
   17.29 +  plus_matrix_def: "A + B = combine_matrix (op +) A B"
   17.30  
   17.31  instance ..
   17.32  
   17.33 @@ -1482,7 +1482,7 @@
   17.34  begin
   17.35  
   17.36  definition
   17.37 -  minus_matrix_def [code del]: "- A = apply_matrix uminus A"
   17.38 +  minus_matrix_def: "- A = apply_matrix uminus A"
   17.39  
   17.40  instance ..
   17.41  
   17.42 @@ -1492,7 +1492,7 @@
   17.43  begin
   17.44  
   17.45  definition
   17.46 -  diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
   17.47 +  diff_matrix_def: "A - B = combine_matrix (op -) A B"
   17.48  
   17.49  instance ..
   17.50  
   17.51 @@ -1502,7 +1502,7 @@
   17.52  begin
   17.53  
   17.54  definition
   17.55 -  times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
   17.56 +  times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"
   17.57  
   17.58  instance ..
   17.59  
   17.60 @@ -1512,7 +1512,7 @@
   17.61  begin
   17.62  
   17.63  definition
   17.64 -  abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
   17.65 +  abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
   17.66  
   17.67  instance ..
   17.68  
    18.1 --- a/src/HOL/NSA/HDeriv.thy	Mon Jul 12 08:58:12 2010 +0200
    18.2 +++ b/src/HOL/NSA/HDeriv.thy	Mon Jul 12 08:58:13 2010 +0200
    18.3 @@ -26,7 +26,7 @@
    18.4  
    18.5  definition
    18.6    increment :: "[real=>real,real,hypreal] => hypreal" where
    18.7 -  [code del]: "increment f x h = (@inc. f NSdifferentiable x &
    18.8 +  "increment f x h = (@inc. f NSdifferentiable x &
    18.9             inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
   18.10  
   18.11  
    19.1 --- a/src/HOL/NSA/HLim.thy	Mon Jul 12 08:58:12 2010 +0200
    19.2 +++ b/src/HOL/NSA/HLim.thy	Mon Jul 12 08:58:13 2010 +0200
    19.3 @@ -16,18 +16,18 @@
    19.4  definition
    19.5    NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
    19.6              ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
    19.7 -  [code del]: "f -- a --NS> L =
    19.8 +  "f -- a --NS> L =
    19.9      (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
   19.10  
   19.11  definition
   19.12    isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
   19.13      --{*NS definition dispenses with limit notions*}
   19.14 -  [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
   19.15 +  "isNSCont f a = (\<forall>y. y @= star_of a -->
   19.16           ( *f* f) y @= star_of (f a))"
   19.17  
   19.18  definition
   19.19    isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
   19.20 -  [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
   19.21 +  "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
   19.22  
   19.23  
   19.24  subsection {* Limits of Functions *}
    20.1 --- a/src/HOL/NSA/HLog.thy	Mon Jul 12 08:58:12 2010 +0200
    20.2 +++ b/src/HOL/NSA/HLog.thy	Mon Jul 12 08:58:13 2010 +0200
    20.3 @@ -20,11 +20,11 @@
    20.4  
    20.5  definition
    20.6    powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
    20.7 -  [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
    20.8 +  [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
    20.9    
   20.10  definition
   20.11    hlog :: "[hypreal,hypreal] => hypreal" where
   20.12 -  [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
   20.13 +  [transfer_unfold]: "hlog a x = starfun2 log a x"
   20.14  
   20.15  lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
   20.16  by (simp add: powhr_def starfun2_star_n)
    21.1 --- a/src/HOL/NSA/HSEQ.thy	Mon Jul 12 08:58:12 2010 +0200
    21.2 +++ b/src/HOL/NSA/HSEQ.thy	Mon Jul 12 08:58:13 2010 +0200
    21.3 @@ -16,7 +16,7 @@
    21.4    NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
    21.5      ("((_)/ ----NS> (_))" [60, 60] 60) where
    21.6      --{*Nonstandard definition of convergence of sequence*}
    21.7 -  [code del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    21.8 +  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    21.9  
   21.10  definition
   21.11    nslim :: "(nat => 'a::real_normed_vector) => 'a" where
   21.12 @@ -31,12 +31,12 @@
   21.13  definition
   21.14    NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
   21.15      --{*Nonstandard definition for bounded sequence*}
   21.16 -  [code del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
   21.17 +  "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
   21.18  
   21.19  definition
   21.20    NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
   21.21      --{*Nonstandard definition*}
   21.22 -  [code del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
   21.23 +  "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
   21.24  
   21.25  subsection {* Limits of Sequences *}
   21.26  
    22.1 --- a/src/HOL/NSA/HSeries.thy	Mon Jul 12 08:58:12 2010 +0200
    22.2 +++ b/src/HOL/NSA/HSeries.thy	Mon Jul 12 08:58:13 2010 +0200
    22.3 @@ -13,7 +13,7 @@
    22.4  
    22.5  definition
    22.6    sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
    22.7 -  [code del]: "sumhr = 
    22.8 +  "sumhr = 
    22.9        (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
   22.10  
   22.11  definition
   22.12 @@ -22,7 +22,7 @@
   22.13  
   22.14  definition
   22.15    NSsummable :: "(nat=>real) => bool" where
   22.16 -  [code del]: "NSsummable f = (\<exists>s. f NSsums s)"
   22.17 +  "NSsummable f = (\<exists>s. f NSsums s)"
   22.18  
   22.19  definition
   22.20    NSsuminf   :: "(nat=>real) => real" where
    23.1 --- a/src/HOL/NSA/HyperDef.thy	Mon Jul 12 08:58:12 2010 +0200
    23.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon Jul 12 08:58:13 2010 +0200
    23.3 @@ -45,7 +45,7 @@
    23.4  begin
    23.5  
    23.6  definition
    23.7 -  star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)"
    23.8 +  star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
    23.9  
   23.10  instance ..
   23.11  
   23.12 @@ -111,7 +111,7 @@
   23.13  
   23.14  definition
   23.15    of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
   23.16 -  [transfer_unfold, code del]: "of_hypreal = *f* of_real"
   23.17 +  [transfer_unfold]: "of_hypreal = *f* of_real"
   23.18  
   23.19  lemma Standard_of_hypreal [simp]:
   23.20    "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
   23.21 @@ -435,7 +435,7 @@
   23.22  subsection{*Powers with Hypernatural Exponents*}
   23.23  
   23.24  definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
   23.25 -  hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
   23.26 +  hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N"
   23.27    (* hypernatural powers of hyperreals *)
   23.28  
   23.29  lemma Standard_hyperpow [simp]:
    24.1 --- a/src/HOL/NSA/HyperNat.thy	Mon Jul 12 08:58:12 2010 +0200
    24.2 +++ b/src/HOL/NSA/HyperNat.thy	Mon Jul 12 08:58:13 2010 +0200
    24.3 @@ -19,7 +19,7 @@
    24.4  
    24.5  definition
    24.6    hSuc :: "hypnat => hypnat" where
    24.7 -  hSuc_def [transfer_unfold, code del]: "hSuc = *f* Suc"
    24.8 +  hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
    24.9  
   24.10  subsection{*Properties Transferred from Naturals*}
   24.11  
   24.12 @@ -366,7 +366,7 @@
   24.13  
   24.14  definition
   24.15    of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
   24.16 -  of_hypnat_def [transfer_unfold, code del]: "of_hypnat = *f* of_nat"
   24.17 +  of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
   24.18  
   24.19  lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
   24.20  by transfer (rule of_nat_0)
    25.1 --- a/src/HOL/NSA/NSA.thy	Mon Jul 12 08:58:12 2010 +0200
    25.2 +++ b/src/HOL/NSA/NSA.thy	Mon Jul 12 08:58:13 2010 +0200
    25.3 @@ -15,15 +15,15 @@
    25.4  
    25.5  definition
    25.6    Infinitesimal  :: "('a::real_normed_vector) star set" where
    25.7 -  [code del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
    25.8 +  "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
    25.9  
   25.10  definition
   25.11    HFinite :: "('a::real_normed_vector) star set" where
   25.12 -  [code del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
   25.13 +  "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
   25.14  
   25.15  definition
   25.16    HInfinite :: "('a::real_normed_vector) star set" where
   25.17 -  [code del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
   25.18 +  "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
   25.19  
   25.20  definition
   25.21    approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "@=" 50) where
   25.22 @@ -56,7 +56,7 @@
   25.23  
   25.24  definition
   25.25    scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
   25.26 -  [transfer_unfold, code del]: "scaleHR = starfun2 scaleR"
   25.27 +  [transfer_unfold]: "scaleHR = starfun2 scaleR"
   25.28  
   25.29  lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
   25.30  by (simp add: hnorm_def)
    26.1 --- a/src/HOL/NSA/NSCA.thy	Mon Jul 12 08:58:12 2010 +0200
    26.2 +++ b/src/HOL/NSA/NSCA.thy	Mon Jul 12 08:58:13 2010 +0200
    26.3 @@ -16,7 +16,7 @@
    26.4  
    26.5  definition --{* standard part map*}
    26.6    stc :: "hcomplex => hcomplex" where 
    26.7 -  [code del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
    26.8 +  "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
    26.9  
   26.10  
   26.11  subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
    27.1 --- a/src/HOL/NSA/NSComplex.thy	Mon Jul 12 08:58:12 2010 +0200
    27.2 +++ b/src/HOL/NSA/NSComplex.thy	Mon Jul 12 08:58:13 2010 +0200
    27.3 @@ -25,11 +25,11 @@
    27.4  
    27.5  definition
    27.6    hRe :: "hcomplex => hypreal" where
    27.7 -  [code del]: "hRe = *f* Re"
    27.8 +  "hRe = *f* Re"
    27.9  
   27.10  definition
   27.11    hIm :: "hcomplex => hypreal" where
   27.12 -  [code del]: "hIm = *f* Im"
   27.13 +  "hIm = *f* Im"
   27.14  
   27.15  
   27.16    (*------ imaginary unit ----------*)
   27.17 @@ -42,22 +42,22 @@
   27.18  
   27.19  definition
   27.20    hcnj :: "hcomplex => hcomplex" where
   27.21 -  [code del]: "hcnj = *f* cnj"
   27.22 +  "hcnj = *f* cnj"
   27.23  
   27.24    (*------------ Argand -------------*)
   27.25  
   27.26  definition
   27.27    hsgn :: "hcomplex => hcomplex" where
   27.28 -  [code del]: "hsgn = *f* sgn"
   27.29 +  "hsgn = *f* sgn"
   27.30  
   27.31  definition
   27.32    harg :: "hcomplex => hypreal" where
   27.33 -  [code del]: "harg = *f* arg"
   27.34 +  "harg = *f* arg"
   27.35  
   27.36  definition
   27.37    (* abbreviation for (cos a + i sin a) *)
   27.38    hcis :: "hypreal => hcomplex" where
   27.39 -  [code del]:"hcis = *f* cis"
   27.40 +  "hcis = *f* cis"
   27.41  
   27.42    (*----- injection from hyperreals -----*)
   27.43  
   27.44 @@ -68,16 +68,16 @@
   27.45  definition
   27.46    (* abbreviation for r*(cos a + i sin a) *)
   27.47    hrcis :: "[hypreal, hypreal] => hcomplex" where
   27.48 -  [code del]: "hrcis = *f2* rcis"
   27.49 +  "hrcis = *f2* rcis"
   27.50  
   27.51    (*------------ e ^ (x + iy) ------------*)
   27.52  definition
   27.53    hexpi :: "hcomplex => hcomplex" where
   27.54 -  [code del]: "hexpi = *f* expi"
   27.55 +  "hexpi = *f* expi"
   27.56  
   27.57  definition
   27.58    HComplex :: "[hypreal,hypreal] => hcomplex" where
   27.59 -  [code del]: "HComplex = *f2* Complex"
   27.60 +  "HComplex = *f2* Complex"
   27.61  
   27.62  lemmas hcomplex_defs [transfer_unfold] =
   27.63    hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
    28.1 --- a/src/HOL/NSA/Star.thy	Mon Jul 12 08:58:12 2010 +0200
    28.2 +++ b/src/HOL/NSA/Star.thy	Mon Jul 12 08:58:13 2010 +0200
    28.3 @@ -17,12 +17,12 @@
    28.4  
    28.5  definition
    28.6    InternalSets :: "'a star set set" where
    28.7 -  [code del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
    28.8 +  "InternalSets = {X. \<exists>As. X = *sn* As}"
    28.9  
   28.10  definition
   28.11    (* nonstandard extension of function *)
   28.12    is_starext  :: "['a star => 'a star, 'a => 'a] => bool" where
   28.13 -  [code del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
   28.14 +  "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
   28.15                          ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
   28.16  
   28.17  definition
   28.18 @@ -32,7 +32,7 @@
   28.19  
   28.20  definition
   28.21    InternalFuns :: "('a star => 'b star) set" where
   28.22 -  [code del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
   28.23 +  "InternalFuns = {X. \<exists>F. X = *fn* F}"
   28.24  
   28.25  
   28.26  (*--------------------------------------------------------
    29.1 --- a/src/HOL/NSA/StarDef.thy	Mon Jul 12 08:58:12 2010 +0200
    29.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Jul 12 08:58:13 2010 +0200
    29.3 @@ -290,7 +290,7 @@
    29.4  subsection {* Internal predicates *}
    29.5  
    29.6  definition unstar :: "bool star \<Rightarrow> bool" where
    29.7 -  [code del]: "unstar b \<longleftrightarrow> b = star_of True"
    29.8 +  "unstar b \<longleftrightarrow> b = star_of True"
    29.9  
   29.10  lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
   29.11  by (simp add: unstar_def star_of_def star_n_eq_iff)
   29.12 @@ -431,7 +431,7 @@
   29.13  begin
   29.14  
   29.15  definition
   29.16 -  star_zero_def [code del]:    "0 \<equiv> star_of 0"
   29.17 +  star_zero_def:    "0 \<equiv> star_of 0"
   29.18  
   29.19  instance ..
   29.20  
   29.21 @@ -441,7 +441,7 @@
   29.22  begin
   29.23  
   29.24  definition
   29.25 -  star_one_def [code del]:     "1 \<equiv> star_of 1"
   29.26 +  star_one_def:     "1 \<equiv> star_of 1"
   29.27  
   29.28  instance ..
   29.29  
   29.30 @@ -451,7 +451,7 @@
   29.31  begin
   29.32  
   29.33  definition
   29.34 -  star_add_def [code del]:     "(op +) \<equiv> *f2* (op +)"
   29.35 +  star_add_def:     "(op +) \<equiv> *f2* (op +)"
   29.36  
   29.37  instance ..
   29.38  
   29.39 @@ -461,7 +461,7 @@
   29.40  begin
   29.41  
   29.42  definition
   29.43 -  star_mult_def [code del]:    "(op *) \<equiv> *f2* (op *)"
   29.44 +  star_mult_def:    "(op *) \<equiv> *f2* (op *)"
   29.45  
   29.46  instance ..
   29.47  
   29.48 @@ -471,7 +471,7 @@
   29.49  begin
   29.50  
   29.51  definition
   29.52 -  star_minus_def [code del]:   "uminus \<equiv> *f* uminus"
   29.53 +  star_minus_def:   "uminus \<equiv> *f* uminus"
   29.54  
   29.55  instance ..
   29.56  
   29.57 @@ -481,7 +481,7 @@
   29.58  begin
   29.59  
   29.60  definition
   29.61 -  star_diff_def [code del]:    "(op -) \<equiv> *f2* (op -)"
   29.62 +  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
   29.63  
   29.64  instance ..
   29.65  
    30.1 --- a/src/HOL/Number_Theory/Primes.thy	Mon Jul 12 08:58:12 2010 +0200
    30.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Jul 12 08:58:13 2010 +0200
    30.3 @@ -45,7 +45,7 @@
    30.4  definition
    30.5    prime_nat :: "nat \<Rightarrow> bool"
    30.6  where
    30.7 -  [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    30.8 +  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    30.9  
   30.10  instance proof qed
   30.11  
   30.12 @@ -58,7 +58,7 @@
   30.13  definition
   30.14    prime_int :: "int \<Rightarrow> bool"
   30.15  where
   30.16 -  [code del]: "prime_int p = prime (nat p)"
   30.17 +  "prime_int p = prime (nat p)"
   30.18  
   30.19  instance proof qed
   30.20  
    31.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Mon Jul 12 08:58:12 2010 +0200
    31.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Mon Jul 12 08:58:13 2010 +0200
    31.3 @@ -17,7 +17,7 @@
    31.4  
    31.5  definition
    31.6    is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
    31.7 -  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    31.8 +  "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    31.9      (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
   31.10  
   31.11  text {* Uniqueness *}
    32.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Mon Jul 12 08:58:12 2010 +0200
    32.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Mon Jul 12 08:58:13 2010 +0200
    32.3 @@ -15,7 +15,7 @@
    32.4  
    32.5  definition
    32.6    prime :: "nat \<Rightarrow> bool" where
    32.7 -  [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    32.8 +  "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    32.9  
   32.10  
   32.11  lemma two_is_prime: "prime 2"
    33.1 --- a/src/HOL/Product_Type.thy	Mon Jul 12 08:58:12 2010 +0200
    33.2 +++ b/src/HOL/Product_Type.thy	Mon Jul 12 08:58:13 2010 +0200
    33.3 @@ -829,7 +829,7 @@
    33.4  *}
    33.5  
    33.6  definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
    33.7 -  [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
    33.8 +  "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
    33.9  
   33.10  lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
   33.11    by (simp add: prod_fun_def)
    34.1 --- a/src/HOL/RealDef.thy	Mon Jul 12 08:58:12 2010 +0200
    34.2 +++ b/src/HOL/RealDef.thy	Mon Jul 12 08:58:13 2010 +0200
    34.3 @@ -751,7 +751,7 @@
    34.4  begin
    34.5  
    34.6  definition
    34.7 -  "(number_of x :: real) = of_int x"
    34.8 +  [code del]: "(number_of x :: real) = of_int x"
    34.9  
   34.10  instance proof
   34.11  qed (rule number_of_real_def)
   34.12 @@ -1498,8 +1498,6 @@
   34.13  
   34.14  subsection{*Numerals and Arithmetic*}
   34.15  
   34.16 -declare number_of_real_def [code del]
   34.17 -
   34.18  lemma [code_unfold_post]:
   34.19    "number_of k = real_of_int (number_of k)"
   34.20    unfolding number_of_is_id number_of_real_def ..
    35.1 --- a/src/HOL/SupInf.thy	Mon Jul 12 08:58:12 2010 +0200
    35.2 +++ b/src/HOL/SupInf.thy	Mon Jul 12 08:58:13 2010 +0200
    35.3 @@ -9,7 +9,7 @@
    35.4  instantiation real :: Sup 
    35.5  begin
    35.6  definition
    35.7 -  Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
    35.8 +  Sup_real_def: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
    35.9  
   35.10  instance ..
   35.11  end
   35.12 @@ -17,7 +17,7 @@
   35.13  instantiation real :: Inf 
   35.14  begin
   35.15  definition
   35.16 -  Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
   35.17 +  Inf_real_def: "Inf (X::real set) == - (Sup (uminus ` X))"
   35.18  
   35.19  instance ..
   35.20  end
    36.1 --- a/src/HOL/ex/Dedekind_Real.thy	Mon Jul 12 08:58:12 2010 +0200
    36.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Mon Jul 12 08:58:13 2010 +0200
    36.3 @@ -19,7 +19,7 @@
    36.4  
    36.5  definition
    36.6    cut :: "rat set => bool" where
    36.7 -  [code del]: "cut A = ({} \<subset> A &
    36.8 +  "cut A = ({} \<subset> A &
    36.9              A < {r. 0 < r} &
   36.10              (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
   36.11  
   36.12 @@ -49,7 +49,7 @@
   36.13  
   36.14  definition
   36.15    psup :: "preal set => preal" where
   36.16 -  [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
   36.17 +  "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
   36.18  
   36.19  definition
   36.20    add_set :: "[rat set,rat set] => rat set" where
   36.21 @@ -57,7 +57,7 @@
   36.22  
   36.23  definition
   36.24    diff_set :: "[rat set,rat set] => rat set" where
   36.25 -  [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
   36.26 +  "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
   36.27  
   36.28  definition
   36.29    mult_set :: "[rat set,rat set] => rat set" where
   36.30 @@ -65,17 +65,17 @@
   36.31  
   36.32  definition
   36.33    inverse_set :: "rat set => rat set" where
   36.34 -  [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
   36.35 +  "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
   36.36  
   36.37  instantiation preal :: "{ord, plus, minus, times, inverse, one}"
   36.38  begin
   36.39  
   36.40  definition
   36.41 -  preal_less_def [code del]:
   36.42 +  preal_less_def:
   36.43      "R < S == Rep_preal R < Rep_preal S"
   36.44  
   36.45  definition
   36.46 -  preal_le_def [code del]:
   36.47 +  preal_le_def:
   36.48      "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
   36.49  
   36.50  definition
   36.51 @@ -1162,7 +1162,7 @@
   36.52  
   36.53  definition
   36.54    realrel   ::  "((preal * preal) * (preal * preal)) set" where
   36.55 -  [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
   36.56 +  "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
   36.57  
   36.58  typedef (Real)  real = "UNIV//realrel"
   36.59    by (auto simp add: quotient_def)
   36.60 @@ -1170,46 +1170,46 @@
   36.61  definition
   36.62    (** these don't use the overloaded "real" function: users don't see them **)
   36.63    real_of_preal :: "preal => real" where
   36.64 -  [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
   36.65 +  "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
   36.66  
   36.67  instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
   36.68  begin
   36.69  
   36.70  definition
   36.71 -  real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
   36.72 +  real_zero_def: "0 = Abs_Real(realrel``{(1, 1)})"
   36.73  
   36.74  definition
   36.75 -  real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
   36.76 +  real_one_def: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
   36.77  
   36.78  definition
   36.79 -  real_add_def [code del]: "z + w =
   36.80 +  real_add_def: "z + w =
   36.81         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
   36.82                   { Abs_Real(realrel``{(x+u, y+v)}) })"
   36.83  
   36.84  definition
   36.85 -  real_minus_def [code del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   36.86 +  real_minus_def: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
   36.87  
   36.88  definition
   36.89 -  real_diff_def [code del]: "r - (s::real) = r + - s"
   36.90 +  real_diff_def: "r - (s::real) = r + - s"
   36.91  
   36.92  definition
   36.93 -  real_mult_def [code del]:
   36.94 +  real_mult_def:
   36.95      "z * w =
   36.96         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
   36.97                   { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
   36.98  
   36.99  definition
  36.100 -  real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
  36.101 +  real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
  36.102  
  36.103  definition
  36.104 -  real_divide_def [code del]: "R / (S::real) = R * inverse S"
  36.105 +  real_divide_def: "R / (S::real) = R * inverse S"
  36.106  
  36.107  definition
  36.108 -  real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
  36.109 +  real_le_def: "z \<le> (w::real) \<longleftrightarrow>
  36.110      (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
  36.111  
  36.112  definition
  36.113 -  real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
  36.114 +  real_less_def: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
  36.115  
  36.116  definition
  36.117    real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
  36.118 @@ -1656,7 +1656,7 @@
  36.119  begin
  36.120  
  36.121  definition
  36.122 -  real_number_of_def [code del]: "(number_of w :: real) = of_int w"
  36.123 +  real_number_of_def: "(number_of w :: real) = of_int w"
  36.124  
  36.125  instance
  36.126    by intro_classes (simp add: real_number_of_def)
    37.1 --- a/src/HOL/ex/Gauge_Integration.thy	Mon Jul 12 08:58:12 2010 +0200
    37.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Mon Jul 12 08:58:13 2010 +0200
    37.3 @@ -28,7 +28,7 @@
    37.4  
    37.5  definition
    37.6    gauge :: "[real set, real => real] => bool" where
    37.7 -  [code del]: "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
    37.8 +  "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
    37.9  
   37.10  
   37.11  subsection {* Gauge-fine divisions *}
   37.12 @@ -259,7 +259,7 @@
   37.13  
   37.14  definition
   37.15    Integral :: "[(real*real),real=>real,real] => bool" where
   37.16 -  [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
   37.17 +  "Integral = (%(a,b) f k. \<forall>e > 0.
   37.18                                 (\<exists>\<delta>. gauge {a .. b} \<delta> &
   37.19                                 (\<forall>D. fine \<delta> (a,b) D -->
   37.20                                           \<bar>rsum D f - k\<bar> < e)))"
    38.1 --- a/src/HOL/ex/Numeral.thy	Mon Jul 12 08:58:12 2010 +0200
    38.2 +++ b/src/HOL/ex/Numeral.thy	Mon Jul 12 08:58:13 2010 +0200
    38.3 @@ -106,16 +106,16 @@
    38.4  begin
    38.5  
    38.6  definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
    38.7 -  [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
    38.8 +  "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
    38.9  
   38.10  definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
   38.11 -  [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
   38.12 +  "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
   38.13  
   38.14  definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
   38.15 -  [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
   38.16 +  "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
   38.17  
   38.18  definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
   38.19 -  [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
   38.20 +  "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
   38.21  
   38.22  instance ..
   38.23  
   38.24 @@ -761,10 +761,10 @@
   38.25  lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
   38.26  
   38.27  definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   38.28 -  [simp, code del]: "sub m n = (of_num m - of_num n)"
   38.29 +  [simp]: "sub m n = (of_num m - of_num n)"
   38.30  
   38.31  definition dup :: "int \<Rightarrow> int" where
   38.32 -  [code del]: "dup k = 2 * k"
   38.33 +  "dup k = 2 * k"
   38.34  
   38.35  lemma Dig_sub [code]:
   38.36    "sub One One = 0"