--- a/src/HOL/Archimedean_Field.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Archimedean_Field.thy Mon Jul 12 08:58:13 2010 +0200
@@ -143,7 +143,7 @@
definition
floor :: "'a::archimedean_field \<Rightarrow> int" where
- [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+ "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
notation (xsymbols)
floor ("\<lfloor>_\<rfloor>")
@@ -274,7 +274,7 @@
definition
ceiling :: "'a::archimedean_field \<Rightarrow> int" where
- [code del]: "ceiling x = - floor (- x)"
+ "ceiling x = - floor (- x)"
notation (xsymbols)
ceiling ("\<lceil>_\<rceil>")
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 12 08:58:13 2010 +0200
@@ -42,7 +42,7 @@
definition
traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
where
-[code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
+ "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
| Node x r \<Rightarrow> (do tl \<leftarrow> Ref.lookup r;
return (Inr tl) done))
(\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
--- a/src/HOL/Library/Char_ord.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Char_ord.thy Mon Jul 12 08:58:13 2010 +0200
@@ -63,11 +63,11 @@
begin
definition
- char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+ char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
definition
- char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+ char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
instance
--- a/src/HOL/Library/ContNotDenum.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Mon Jul 12 08:58:13 2010 +0200
@@ -402,7 +402,6 @@
(f (Suc n)) \<notin> e)
)"
-declare newInt.simps [code del]
subsubsection {* Properties *}
--- a/src/HOL/Library/Dlist.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Jul 12 08:58:13 2010 +0200
@@ -23,7 +23,7 @@
text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
- [code del]: "Dlist xs = Abs_dlist (remdups xs)"
+ "Dlist xs = Abs_dlist (remdups xs)"
lemma distinct_list_of_dlist [simp]:
"distinct (list_of_dlist dxs)"
--- a/src/HOL/Library/Enum.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Enum.thy Mon Jul 12 08:58:13 2010 +0200
@@ -149,7 +149,7 @@
begin
definition
- [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)"
+ "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
instance proof
show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
@@ -278,7 +278,7 @@
begin
definition
- [code del]: "enum = map (split Char) (product enum enum)"
+ "enum = map (split Char) (product enum enum)"
lemma enum_chars [code]:
"enum = chars"
--- a/src/HOL/Library/Fraction_Field.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Mon Jul 12 08:58:13 2010 +0200
@@ -69,7 +69,7 @@
definition
Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
- [code del]: "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
+ "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
code_datatype Fract
@@ -93,13 +93,13 @@
begin
definition
- Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
+ Zero_fract_def [code_unfold]: "0 = Fract 0 1"
definition
- One_fract_def [code, code_unfold]: "1 = Fract 1 1"
+ One_fract_def [code_unfold]: "1 = Fract 1 1"
definition
- add_fract_def [code del]:
+ add_fract_def:
"q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
@@ -115,7 +115,7 @@
qed
definition
- minus_fract_def [code del]:
+ minus_fract_def:
"- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})"
lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
@@ -129,7 +129,7 @@
by (cases "b = 0") (simp_all add: eq_fract)
definition
- diff_fract_def [code del]: "q - r = q + - (r::'a fract)"
+ diff_fract_def: "q - r = q + - (r::'a fract)"
lemma diff_fract [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -137,7 +137,7 @@
using assms by (simp add: diff_fract_def diff_minus)
definition
- mult_fract_def [code del]:
+ mult_fract_def:
"q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
fractrel``{(fst x * fst y, snd x * snd y)})"
@@ -236,7 +236,7 @@
begin
definition
- inverse_fract_def [code del]:
+ inverse_fract_def:
"inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.
fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
@@ -250,7 +250,7 @@
qed
definition
- divide_fract_def [code del]: "q / r = q * inverse (r:: 'a fract)"
+ divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
by (simp add: divide_fract_def)
@@ -318,12 +318,12 @@
begin
definition
- le_fract_def [code del]:
+ le_fract_def:
"q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
{(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
definition
- less_fract_def [code del]: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
+ less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
lemma le_fract [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
--- a/src/HOL/Library/Fset.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Fset.thy Mon Jul 12 08:58:13 2010 +0200
@@ -124,10 +124,10 @@
begin
definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where
- [simp, code del]: "Inf_fset As = Fset (Inf (image member As))"
+ [simp]: "Inf_fset As = Fset (Inf (image member As))"
definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where
- [simp, code del]: "Sup_fset As = Fset (Sup (image member As))"
+ [simp]: "Sup_fset As = Fset (Sup (image member As))"
instance proof
qed (auto simp add: le_fun_def le_bool_def)
--- a/src/HOL/Library/List_lexord.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/List_lexord.thy Mon Jul 12 08:58:13 2010 +0200
@@ -62,10 +62,10 @@
begin
definition
- [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+ "(inf \<Colon> 'a list \<Rightarrow> _) = min"
definition
- [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
+ "(sup \<Colon> 'a list \<Rightarrow> _) = max"
instance
by intro_classes
--- a/src/HOL/Library/Multiset.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Jul 12 08:58:13 2010 +0200
@@ -978,11 +978,11 @@
subsubsection {* Well-foundedness *}
definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
- [code del]: "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
+ "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
(\<forall>b. b :# K --> (b, a) \<in> r)}"
definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
- [code del]: "mult r = (mult1 r)\<^sup>+"
+ "mult r = (mult1 r)\<^sup>+"
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
by (simp add: mult1_def)
@@ -1498,7 +1498,7 @@
by auto
definition "ms_strict = mult pair_less"
-definition [code del]: "ms_weak = ms_strict \<union> Id"
+definition "ms_weak = ms_strict \<union> Id"
lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
--- a/src/HOL/Library/Nat_Infinity.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Jul 12 08:58:13 2010 +0200
@@ -126,7 +126,7 @@
begin
definition
- [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)))"
+ "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
lemma plus_inat_simps [simp, code]:
"Fin m + Fin n = Fin (m + n)"
@@ -177,7 +177,7 @@
begin
definition
- times_inat_def [code del]:
+ times_inat_def:
"m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
(case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
@@ -238,11 +238,11 @@
begin
definition
- [code del]: "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
+ "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
| \<infinity> \<Rightarrow> True)"
definition
- [code del]: "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
+ "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
| \<infinity> \<Rightarrow> False)"
lemma inat_ord_simps [simp]:
--- a/src/HOL/Library/Option_ord.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Option_ord.thy Mon Jul 12 08:58:13 2010 +0200
@@ -12,10 +12,10 @@
begin
definition less_eq_option where
- [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))"
+ "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))"
definition less_option where
- [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))"
+ "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
lemma less_eq_option_None [simp]: "None \<le> x"
by (simp add: less_eq_option_def)
--- a/src/HOL/Library/Polynomial.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Jul 12 08:58:13 2010 +0200
@@ -98,7 +98,7 @@
definition
pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
where
- [code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"
+ "pCons a p = Abs_poly (nat_case a (coeff p))"
syntax
"_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]")
@@ -209,7 +209,7 @@
function
poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"
where
- poly_rec_pCons_eq_if [simp del, code del]:
+ poly_rec_pCons_eq_if [simp del]:
"poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"
by (case_tac x, rename_tac q, case_tac q, auto)
@@ -266,7 +266,7 @@
begin
definition
- plus_poly_def [code del]:
+ plus_poly_def:
"p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"
lemma Poly_add:
@@ -305,11 +305,11 @@
begin
definition
- uminus_poly_def [code del]:
+ uminus_poly_def:
"- p = Abs_poly (\<lambda>n. - coeff p n)"
definition
- minus_poly_def [code del]:
+ minus_poly_def:
"p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"
lemma Poly_minus:
@@ -512,7 +512,7 @@
begin
definition
- times_poly_def [code del]:
+ times_poly_def:
"p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"
lemma mult_poly_0_left: "(0::'a poly) * q = 0"
@@ -736,20 +736,16 @@
begin
definition
- [code del]:
- "x < y \<longleftrightarrow> pos_poly (y - x)"
+ "x < y \<longleftrightarrow> pos_poly (y - x)"
definition
- [code del]:
- "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
+ "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
definition
- [code del]:
- "abs (x::'a poly) = (if x < 0 then - x else x)"
+ "abs (x::'a poly) = (if x < 0 then - x else x)"
definition
- [code del]:
- "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
+ "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
instance proof
fix x y :: "'a poly"
@@ -818,7 +814,6 @@
definition
pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
where
- [code del]:
"pdivmod_rel x y q r \<longleftrightarrow>
x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
@@ -943,10 +938,10 @@
begin
definition div_poly where
- [code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
+ "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
definition mod_poly where
- [code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
+ "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
lemma div_poly_eq:
"pdivmod_rel x y q r \<Longrightarrow> x div y = q"
@@ -1133,7 +1128,7 @@
by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
(auto dest: degree_mod_less)
-declare poly_gcd.simps [simp del, code del]
+declare poly_gcd.simps [simp del]
lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x"
and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
@@ -1287,7 +1282,7 @@
definition
synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
-where [code del]:
+where
"synthetic_divmod p c =
poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p"
@@ -1442,7 +1437,6 @@
definition
order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
where
- [code del]:
"order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
lemma coeff_linear_power:
@@ -1514,7 +1508,7 @@
instantiation poly :: ("{zero,eq}") eq
begin
-definition [code del]:
+definition
"eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
instance
@@ -1574,7 +1568,7 @@
definition
pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
where
- [code del]: "pdivmod x y = (x div y, x mod y)"
+ "pdivmod x y = (x div y, x mod y)"
lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
unfolding pdivmod_def by simp
--- a/src/HOL/Library/Product_ord.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Product_ord.thy Mon Jul 12 08:58:13 2010 +0200
@@ -12,10 +12,10 @@
begin
definition
- 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"
+ prod_le_def: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
definition
- prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
+ prod_less_def: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
instance ..
--- a/src/HOL/Library/Sublist_Order.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Sublist_Order.thy Mon Jul 12 08:58:13 2010 +0200
@@ -26,7 +26,7 @@
| take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
definition
- [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+ "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
instance proof qed
--- a/src/HOL/Library/Univ_Poly.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Mon Jul 12 08:58:13 2010 +0200
@@ -71,7 +71,7 @@
definition (in semiring_0)
divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "divides" 70) where
- [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
+ "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
--{*order of a polynomial*}
definition (in ring_1) order :: "'a => 'a list => nat" where
--- a/src/HOL/Matrix/Matrix.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Matrix/Matrix.thy Mon Jul 12 08:58:13 2010 +0200
@@ -776,7 +776,7 @@
instantiation matrix :: (zero) zero
begin
-definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
+definition zero_matrix_def: "0 = Abs_matrix (\<lambda>j i. 0)"
instance ..
@@ -1459,9 +1459,9 @@
instantiation matrix :: ("{lattice, zero}") lattice
begin
-definition [code del]: "inf = combine_matrix inf"
+definition "inf = combine_matrix inf"
-definition [code del]: "sup = combine_matrix sup"
+definition "sup = combine_matrix sup"
instance
by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
@@ -1472,7 +1472,7 @@
begin
definition
- plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
+ plus_matrix_def: "A + B = combine_matrix (op +) A B"
instance ..
@@ -1482,7 +1482,7 @@
begin
definition
- minus_matrix_def [code del]: "- A = apply_matrix uminus A"
+ minus_matrix_def: "- A = apply_matrix uminus A"
instance ..
@@ -1492,7 +1492,7 @@
begin
definition
- diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
+ diff_matrix_def: "A - B = combine_matrix (op -) A B"
instance ..
@@ -1502,7 +1502,7 @@
begin
definition
- times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
+ times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"
instance ..
@@ -1512,7 +1512,7 @@
begin
definition
- abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
+ abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
instance ..
--- a/src/HOL/NSA/HDeriv.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/HDeriv.thy Mon Jul 12 08:58:13 2010 +0200
@@ -26,7 +26,7 @@
definition
increment :: "[real=>real,real,hypreal] => hypreal" where
- [code del]: "increment f x h = (@inc. f NSdifferentiable x &
+ "increment f x h = (@inc. f NSdifferentiable x &
inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
--- a/src/HOL/NSA/HLim.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/HLim.thy Mon Jul 12 08:58:13 2010 +0200
@@ -16,18 +16,18 @@
definition
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
- [code del]: "f -- a --NS> L =
+ "f -- a --NS> L =
(\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
definition
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
--{*NS definition dispenses with limit notions*}
- [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
+ "isNSCont f a = (\<forall>y. y @= star_of a -->
( *f* f) y @= star_of (f a))"
definition
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+ "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
subsection {* Limits of Functions *}
--- a/src/HOL/NSA/HLog.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/HLog.thy Mon Jul 12 08:58:13 2010 +0200
@@ -20,11 +20,11 @@
definition
powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
- [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
+ [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
definition
hlog :: "[hypreal,hypreal] => hypreal" where
- [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
+ [transfer_unfold]: "hlog a x = starfun2 log a x"
lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
by (simp add: powhr_def starfun2_star_n)
--- a/src/HOL/NSA/HSEQ.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/HSEQ.thy Mon Jul 12 08:58:13 2010 +0200
@@ -16,7 +16,7 @@
NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ ----NS> (_))" [60, 60] 60) where
--{*Nonstandard definition of convergence of sequence*}
- [code del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+ "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
definition
nslim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -31,12 +31,12 @@
definition
NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
--{*Nonstandard definition for bounded sequence*}
- [code del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+ "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
definition
NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
--{*Nonstandard definition*}
- [code del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+ "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
subsection {* Limits of Sequences *}
--- a/src/HOL/NSA/HSeries.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/HSeries.thy Mon Jul 12 08:58:13 2010 +0200
@@ -13,7 +13,7 @@
definition
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
- [code del]: "sumhr =
+ "sumhr =
(%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
definition
@@ -22,7 +22,7 @@
definition
NSsummable :: "(nat=>real) => bool" where
- [code del]: "NSsummable f = (\<exists>s. f NSsums s)"
+ "NSsummable f = (\<exists>s. f NSsums s)"
definition
NSsuminf :: "(nat=>real) => real" where
--- a/src/HOL/NSA/HyperDef.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon Jul 12 08:58:13 2010 +0200
@@ -45,7 +45,7 @@
begin
definition
- star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)"
+ star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
instance ..
@@ -111,7 +111,7 @@
definition
of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
- [transfer_unfold, code del]: "of_hypreal = *f* of_real"
+ [transfer_unfold]: "of_hypreal = *f* of_real"
lemma Standard_of_hypreal [simp]:
"r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
@@ -435,7 +435,7 @@
subsection{*Powers with Hypernatural Exponents*}
definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
- hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
+ hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N"
(* hypernatural powers of hyperreals *)
lemma Standard_hyperpow [simp]:
--- a/src/HOL/NSA/HyperNat.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/HyperNat.thy Mon Jul 12 08:58:13 2010 +0200
@@ -19,7 +19,7 @@
definition
hSuc :: "hypnat => hypnat" where
- hSuc_def [transfer_unfold, code del]: "hSuc = *f* Suc"
+ hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
subsection{*Properties Transferred from Naturals*}
@@ -366,7 +366,7 @@
definition
of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
- of_hypnat_def [transfer_unfold, code del]: "of_hypnat = *f* of_nat"
+ of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
by transfer (rule of_nat_0)
--- a/src/HOL/NSA/NSA.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/NSA.thy Mon Jul 12 08:58:13 2010 +0200
@@ -15,15 +15,15 @@
definition
Infinitesimal :: "('a::real_normed_vector) star set" where
- [code del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
+ "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
definition
HFinite :: "('a::real_normed_vector) star set" where
- [code del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
+ "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
definition
HInfinite :: "('a::real_normed_vector) star set" where
- [code del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
+ "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
definition
approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where
@@ -56,7 +56,7 @@
definition
scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
- [transfer_unfold, code del]: "scaleHR = starfun2 scaleR"
+ [transfer_unfold]: "scaleHR = starfun2 scaleR"
lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
by (simp add: hnorm_def)
--- a/src/HOL/NSA/NSCA.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/NSCA.thy Mon Jul 12 08:58:13 2010 +0200
@@ -16,7 +16,7 @@
definition --{* standard part map*}
stc :: "hcomplex => hcomplex" where
- [code del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
+ "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
--- a/src/HOL/NSA/NSComplex.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/NSComplex.thy Mon Jul 12 08:58:13 2010 +0200
@@ -25,11 +25,11 @@
definition
hRe :: "hcomplex => hypreal" where
- [code del]: "hRe = *f* Re"
+ "hRe = *f* Re"
definition
hIm :: "hcomplex => hypreal" where
- [code del]: "hIm = *f* Im"
+ "hIm = *f* Im"
(*------ imaginary unit ----------*)
@@ -42,22 +42,22 @@
definition
hcnj :: "hcomplex => hcomplex" where
- [code del]: "hcnj = *f* cnj"
+ "hcnj = *f* cnj"
(*------------ Argand -------------*)
definition
hsgn :: "hcomplex => hcomplex" where
- [code del]: "hsgn = *f* sgn"
+ "hsgn = *f* sgn"
definition
harg :: "hcomplex => hypreal" where
- [code del]: "harg = *f* arg"
+ "harg = *f* arg"
definition
(* abbreviation for (cos a + i sin a) *)
hcis :: "hypreal => hcomplex" where
- [code del]:"hcis = *f* cis"
+ "hcis = *f* cis"
(*----- injection from hyperreals -----*)
@@ -68,16 +68,16 @@
definition
(* abbreviation for r*(cos a + i sin a) *)
hrcis :: "[hypreal, hypreal] => hcomplex" where
- [code del]: "hrcis = *f2* rcis"
+ "hrcis = *f2* rcis"
(*------------ e ^ (x + iy) ------------*)
definition
hexpi :: "hcomplex => hcomplex" where
- [code del]: "hexpi = *f* expi"
+ "hexpi = *f* expi"
definition
HComplex :: "[hypreal,hypreal] => hcomplex" where
- [code del]: "HComplex = *f2* Complex"
+ "HComplex = *f2* Complex"
lemmas hcomplex_defs [transfer_unfold] =
hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
--- a/src/HOL/NSA/Star.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/Star.thy Mon Jul 12 08:58:13 2010 +0200
@@ -17,12 +17,12 @@
definition
InternalSets :: "'a star set set" where
- [code del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
+ "InternalSets = {X. \<exists>As. X = *sn* As}"
definition
(* nonstandard extension of function *)
is_starext :: "['a star => 'a star, 'a => 'a] => bool" where
- [code del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
+ "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
definition
@@ -32,7 +32,7 @@
definition
InternalFuns :: "('a star => 'b star) set" where
- [code del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
+ "InternalFuns = {X. \<exists>F. X = *fn* F}"
(*--------------------------------------------------------
--- a/src/HOL/NSA/StarDef.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Jul 12 08:58:13 2010 +0200
@@ -290,7 +290,7 @@
subsection {* Internal predicates *}
definition unstar :: "bool star \<Rightarrow> bool" where
- [code del]: "unstar b \<longleftrightarrow> b = star_of True"
+ "unstar b \<longleftrightarrow> b = star_of True"
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
by (simp add: unstar_def star_of_def star_n_eq_iff)
@@ -431,7 +431,7 @@
begin
definition
- star_zero_def [code del]: "0 \<equiv> star_of 0"
+ star_zero_def: "0 \<equiv> star_of 0"
instance ..
@@ -441,7 +441,7 @@
begin
definition
- star_one_def [code del]: "1 \<equiv> star_of 1"
+ star_one_def: "1 \<equiv> star_of 1"
instance ..
@@ -451,7 +451,7 @@
begin
definition
- star_add_def [code del]: "(op +) \<equiv> *f2* (op +)"
+ star_add_def: "(op +) \<equiv> *f2* (op +)"
instance ..
@@ -461,7 +461,7 @@
begin
definition
- star_mult_def [code del]: "(op *) \<equiv> *f2* (op *)"
+ star_mult_def: "(op *) \<equiv> *f2* (op *)"
instance ..
@@ -471,7 +471,7 @@
begin
definition
- star_minus_def [code del]: "uminus \<equiv> *f* uminus"
+ star_minus_def: "uminus \<equiv> *f* uminus"
instance ..
@@ -481,7 +481,7 @@
begin
definition
- star_diff_def [code del]: "(op -) \<equiv> *f2* (op -)"
+ star_diff_def: "(op -) \<equiv> *f2* (op -)"
instance ..
--- a/src/HOL/Number_Theory/Primes.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Mon Jul 12 08:58:13 2010 +0200
@@ -45,7 +45,7 @@
definition
prime_nat :: "nat \<Rightarrow> bool"
where
- [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+ "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
instance proof qed
@@ -58,7 +58,7 @@
definition
prime_int :: "int \<Rightarrow> bool"
where
- [code del]: "prime_int p = prime (nat p)"
+ "prime_int p = prime (nat p)"
instance proof qed
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Mon Jul 12 08:58:13 2010 +0200
@@ -17,7 +17,7 @@
definition
is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
- [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
+ "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
(\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
text {* Uniqueness *}
--- a/src/HOL/Old_Number_Theory/Primes.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy Mon Jul 12 08:58:13 2010 +0200
@@ -15,7 +15,7 @@
definition
prime :: "nat \<Rightarrow> bool" where
- [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+ "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
lemma two_is_prime: "prime 2"
--- a/src/HOL/Product_Type.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Product_Type.thy Mon Jul 12 08:58:13 2010 +0200
@@ -829,7 +829,7 @@
*}
definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
- [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
+ "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
by (simp add: prod_fun_def)
--- a/src/HOL/RealDef.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/RealDef.thy Mon Jul 12 08:58:13 2010 +0200
@@ -751,7 +751,7 @@
begin
definition
- "(number_of x :: real) = of_int x"
+ [code del]: "(number_of x :: real) = of_int x"
instance proof
qed (rule number_of_real_def)
@@ -1498,8 +1498,6 @@
subsection{*Numerals and Arithmetic*}
-declare number_of_real_def [code del]
-
lemma [code_unfold_post]:
"number_of k = real_of_int (number_of k)"
unfolding number_of_is_id number_of_real_def ..
--- a/src/HOL/SupInf.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/SupInf.thy Mon Jul 12 08:58:13 2010 +0200
@@ -9,7 +9,7 @@
instantiation real :: Sup
begin
definition
- Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
+ Sup_real_def: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
instance ..
end
@@ -17,7 +17,7 @@
instantiation real :: Inf
begin
definition
- Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
+ Inf_real_def: "Inf (X::real set) == - (Sup (uminus ` X))"
instance ..
end
--- a/src/HOL/ex/Dedekind_Real.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Mon Jul 12 08:58:13 2010 +0200
@@ -19,7 +19,7 @@
definition
cut :: "rat set => bool" where
- [code del]: "cut A = ({} \<subset> A &
+ "cut A = ({} \<subset> A &
A < {r. 0 < r} &
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
@@ -49,7 +49,7 @@
definition
psup :: "preal set => preal" where
- [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
+ "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
definition
add_set :: "[rat set,rat set] => rat set" where
@@ -57,7 +57,7 @@
definition
diff_set :: "[rat set,rat set] => rat set" where
- [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+ "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
definition
mult_set :: "[rat set,rat set] => rat set" where
@@ -65,17 +65,17 @@
definition
inverse_set :: "rat set => rat set" where
- [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+ "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
instantiation preal :: "{ord, plus, minus, times, inverse, one}"
begin
definition
- preal_less_def [code del]:
+ preal_less_def:
"R < S == Rep_preal R < Rep_preal S"
definition
- preal_le_def [code del]:
+ preal_le_def:
"R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
definition
@@ -1162,7 +1162,7 @@
definition
realrel :: "((preal * preal) * (preal * preal)) set" where
- [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
typedef (Real) real = "UNIV//realrel"
by (auto simp add: quotient_def)
@@ -1170,46 +1170,46 @@
definition
(** these don't use the overloaded "real" function: users don't see them **)
real_of_preal :: "preal => real" where
- [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
+ "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
begin
definition
- real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
+ real_zero_def: "0 = Abs_Real(realrel``{(1, 1)})"
definition
- real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
+ real_one_def: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
definition
- real_add_def [code del]: "z + w =
+ real_add_def: "z + w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x+u, y+v)}) })"
definition
- real_minus_def [code del]: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+ real_minus_def: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
definition
- real_diff_def [code del]: "r - (s::real) = r + - s"
+ real_diff_def: "r - (s::real) = r + - s"
definition
- real_mult_def [code del]:
+ real_mult_def:
"z * w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
definition
- real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
+ real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
definition
- real_divide_def [code del]: "R / (S::real) = R * inverse S"
+ real_divide_def: "R / (S::real) = R * inverse S"
definition
- real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
+ real_le_def: "z \<le> (w::real) \<longleftrightarrow>
(\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
definition
- real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+ real_less_def: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
definition
real_abs_def: "abs (r::real) = (if r < 0 then - r else r)"
@@ -1656,7 +1656,7 @@
begin
definition
- real_number_of_def [code del]: "(number_of w :: real) = of_int w"
+ real_number_of_def: "(number_of w :: real) = of_int w"
instance
by intro_classes (simp add: real_number_of_def)
--- a/src/HOL/ex/Gauge_Integration.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Mon Jul 12 08:58:13 2010 +0200
@@ -28,7 +28,7 @@
definition
gauge :: "[real set, real => real] => bool" where
- [code del]: "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
+ "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
subsection {* Gauge-fine divisions *}
@@ -259,7 +259,7 @@
definition
Integral :: "[(real*real),real=>real,real] => bool" where
- [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
+ "Integral = (%(a,b) f k. \<forall>e > 0.
(\<exists>\<delta>. gauge {a .. b} \<delta> &
(\<forall>D. fine \<delta> (a,b) D -->
\<bar>rsum D f - k\<bar> < e)))"
--- a/src/HOL/ex/Numeral.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Mon Jul 12 08:58:13 2010 +0200
@@ -106,16 +106,16 @@
begin
definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
- [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
+ "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
- [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
+ "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
- [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
+ "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
- [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
+ "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
instance ..
@@ -761,10 +761,10 @@
lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
- [simp, code del]: "sub m n = (of_num m - of_num n)"
+ [simp]: "sub m n = (of_num m - of_num n)"
definition dup :: "int \<Rightarrow> int" where
- [code del]: "dup k = 2 * k"
+ "dup k = 2 * k"
lemma Dig_sub [code]:
"sub One One = 0"