# HG changeset patch # User haftmann # Date 1278917893 -7200 # Node ID 26bdfb7b680b1096f8c26e1921717ef89751ed71 # Parent 3489daf839d51edc4a0df05f1032ec49f1bce222 dropped superfluous [code del]s diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Archimedean_Field.thy --- 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 \ int" where - [code del]: "floor x = (THE z. of_int z \ x \ x < of_int (z + 1))" + "floor x = (THE z. of_int z \ x \ x < of_int (z + 1))" notation (xsymbols) floor ("\_\") @@ -274,7 +274,7 @@ definition ceiling :: "'a::archimedean_field \ int" where - [code del]: "ceiling x = - floor (- x)" + "ceiling x = - floor (- x)" notation (xsymbols) ceiling ("\_\") diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- 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\heap node \ 'a list Heap" where -[code del]: "traverse = MREC (\n. case n of Empty \ return (Inl []) + "traverse = MREC (\n. case n of Empty \ return (Inl []) | Node x r \ (do tl \ Ref.lookup r; return (Inr tl) done)) (\n tl xs. case n of Empty \ undefined diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Char_ord.thy --- 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 \ c2 \ (case c1 of Char n1 m1 \ case c2 of Char n2 m2 \ + char_less_eq_def: "c1 \ c2 \ (case c1 of Char n1 m1 \ case c2 of Char n2 m2 \ n1 < n2 \ n1 = n2 \ m1 \ m2)" definition - char_less_def [code del]: "c1 < c2 \ (case c1 of Char n1 m1 \ case c2 of Char n2 m2 \ + char_less_def: "c1 < c2 \ (case c1 of Char n1 m1 \ case c2 of Char n2 m2 \ n1 < n2 \ n1 = n2 \ m1 < m2)" instance diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/ContNotDenum.thy --- 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)) \ e) )" -declare newInt.simps [code del] subsubsection {* Properties *} diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Dlist.thy --- 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 \ '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)" diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Enum.thy --- 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 (\ys. the o map_of (zip (enum\'a list) ys)) (n_lists (length (enum\'a\enum list)) enum)" + "enum = map (\ys. the o map_of (zip (enum\'a list) ys)) (n_lists (length (enum\'a\enum list)) enum)" instance proof show "UNIV = set (enum \ ('a \ '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" diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Fraction_Field.thy --- 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 \ 'a \ '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 (\x \ Rep_fract q. \y \ 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 (\x \ 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 \ 0" and "d \ 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 (\x \ Rep_fract q. \y \ 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 (\x \ 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 \ r \ contents (\x \ Rep_fract q. \y \ Rep_fract r. {(fst x * snd y)*(snd x * snd y) \ (fst y * snd x)*(snd x * snd y)})" definition - less_fract_def [code del]: "z < (w::'a fract) \ z \ w \ \ w \ z" + less_fract_def: "z < (w::'a fract) \ z \ w \ \ w \ z" lemma le_fract [simp]: assumes "b \ 0" and "d \ 0" diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Fset.thy --- 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 \ '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 \ '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) diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/List_lexord.thy --- 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 \ 'a list \ _) = min" + "(inf \ 'a list \ _) = min" definition - [code del]: "(sup \ 'a list \ _) = max" + "(sup \ 'a list \ _) = max" instance by intro_classes diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Multiset.thy --- 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 \ 'a) set => ('a multiset \ 'a multiset) set" where - [code del]: "mult1 r = {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ + "mult1 r = {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ (\b. b :# K --> (b, a) \ r)}" definition mult :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" where - [code del]: "mult r = (mult1 r)\<^sup>+" + "mult r = (mult1 r)\<^sup>+" lemma not_less_empty [iff]: "(M, {#}) \ 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 \ Id" +definition "ms_weak = ms_strict \ Id" lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)" unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Nat_Infinity.thy --- 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 \ \ \ | Fin m \ (case n of \ \ \ | Fin n \ Fin (m + n)))" + "m + n = (case m of \ \ \ | Fin m \ (case n of \ \ \ | Fin n \ 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 \ \ if n = 0 then 0 else \ | Fin m \ (case n of \ \ if m = 0 then 0 else \ | Fin n \ Fin (m * n)))" @@ -238,11 +238,11 @@ begin definition - [code del]: "m \ n = (case n of Fin n1 \ (case m of Fin m1 \ m1 \ n1 | \ \ False) + "m \ n = (case n of Fin n1 \ (case m of Fin m1 \ m1 \ n1 | \ \ False) | \ \ True)" definition - [code del]: "m < n = (case m of Fin m1 \ (case n of Fin n1 \ m1 < n1 | \ \ True) + "m < n = (case m of Fin m1 \ (case n of Fin n1 \ m1 < n1 | \ \ True) | \ \ False)" lemma inat_ord_simps [simp]: diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Option_ord.thy --- 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 \ y \ (case x of None \ True | Some x \ (case y of None \ False | Some y \ x \ y))" + "x \ y \ (case x of None \ True | Some x \ (case y of None \ False | Some y \ x \ y))" definition less_option where - [code del]: "x < y \ (case y of None \ False | Some y \ (case x of None \ True | Some x \ x < y))" + "x < y \ (case y of None \ False | Some y \ (case x of None \ True | Some x \ x < y))" lemma less_eq_option_None [simp]: "None \ x" by (simp add: less_eq_option_def) diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Polynomial.thy --- 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 \ 'a poly \ '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 \ 'a poly" ("[:(_):]") @@ -209,7 +209,7 @@ function poly_rec :: "'b \ ('a::zero \ 'a poly \ 'b \ 'b) \ 'a poly \ '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 (\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 (\n. - coeff p n)" definition - minus_poly_def [code del]: + minus_poly_def: "p - q = Abs_poly (\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 (\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 \ pos_poly (y - x)" + "x < y \ pos_poly (y - x)" definition - [code del]: - "x \ y \ x = y \ pos_poly (y - x)" + "x \ y \ x = y \ 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 \ 'a poly \ 'a poly \ 'a poly \ bool" where - [code del]: "pdivmod_rel x y q r \ x = q * y + r \ (if y = 0 then q = 0 else r = 0 \ degree r < degree y)" @@ -943,10 +938,10 @@ begin definition div_poly where - [code del]: "x div y = (THE q. \r. pdivmod_rel x y q r)" + "x div y = (THE q. \r. pdivmod_rel x y q r)" definition mod_poly where - [code del]: "x mod y = (THE r. \q. pdivmod_rel x y q r)" + "x mod y = (THE r. \q. pdivmod_rel x y q r)" lemma div_poly_eq: "pdivmod_rel x y q r \ x div y = q" @@ -1133,7 +1128,7 @@ by (relation "measure (\(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 \ 'a \ 'a poly \ 'a" -where [code del]: +where "synthetic_divmod p c = poly_rec (0, 0) (\a p (q, r). (pCons r q, a + c * r)) p" @@ -1442,7 +1437,6 @@ definition order :: "'a::idom \ 'a poly \ nat" where - [code del]: "order a p = (LEAST n. \ [:-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 \ p = q" instance @@ -1574,7 +1568,7 @@ definition pdivmod :: "'a::field poly \ 'a poly \ 'a poly \ '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 diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Product_ord.thy --- 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 \ y \ fst x < fst y \ fst x \ fst y \ snd x \ snd y" + prod_le_def: "x \ y \ fst x < fst y \ fst x \ fst y \ snd x \ snd y" definition - prod_less_def [code del]: "x < y \ fst x < fst y \ fst x \ fst y \ snd x < snd y" + prod_less_def: "x < y \ fst x < fst y \ fst x \ fst y \ snd x < snd y" instance .. diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Sublist_Order.thy --- 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 \ xs \ x # ys \ x # xs" definition - [code del]: "(xs \ 'a list) < ys \ xs \ ys \ \ ys \ xs" + "(xs \ 'a list) < ys \ xs \ ys \ \ ys \ xs" instance proof qed diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/Univ_Poly.thy --- 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 \ 'a list \ bool" (infixl "divides" 70) where - [code del]: "p1 divides p2 = (\q. poly p2 = poly(p1 *** q))" + "p1 divides p2 = (\q. poly p2 = poly(p1 *** q))" --{*order of a polynomial*} definition (in ring_1) order :: "'a => 'a list => nat" where diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Matrix/Matrix.thy --- 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 (\j i. 0)" +definition zero_matrix_def: "0 = Abs_matrix (\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 \ 'a matrix) = sup A (- A)" + abs_matrix_def: "abs (A \ 'a matrix) = sup A (- A)" instance .. diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/HDeriv.thy --- 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))" diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/HLim.thy --- 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 = (\x. (x \ 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 = (\y. y @= star_of a --> + "isNSCont f a = (\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 = (\x y. x @= y --> ( *f* f) x @= ( *f* f) y)" + "isNSUCont f = (\x y. x @= y --> ( *f* f) x @= ( *f* f) y)" subsection {* Limits of Functions *} diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/HLog.thy --- 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) diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/HSEQ.thy --- 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 = (\N \ HNatInfinite. ( *f* X) N \ star_of L)" + "X ----NS> L = (\N \ HNatInfinite. ( *f* X) N \ 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 = (\N \ HNatInfinite. ( *f* X) N : HFinite)" + "NSBseq X = (\N \ HNatInfinite. ( *f* X) N : HFinite)" definition NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where --{*Nonstandard definition*} - [code del]: "NSCauchy X = (\M \ HNatInfinite. \N \ HNatInfinite. ( *f* X) M \ ( *f* X) N)" + "NSCauchy X = (\M \ HNatInfinite. \N \ HNatInfinite. ( *f* X) M \ ( *f* X) N)" subsection {* Limits of Sequences *} diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/HSeries.thy --- 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..real) => bool" where - [code del]: "NSsummable f = (\s. f NSsums s)" + "NSsummable f = (\s. f NSsums s)" definition NSsuminf :: "(nat=>real) => real" where diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/HyperDef.thy --- 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 \ *f* (scaleR r)" + star_scaleR_def [transfer_unfold]: "scaleR r \ *f* (scaleR r)" instance .. @@ -111,7 +111,7 @@ definition of_hypreal :: "hypreal \ '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 \ Standard \ of_hypreal r \ Standard" @@ -435,7 +435,7 @@ subsection{*Powers with Hypernatural Exponents*} definition pow :: "['a::power star, nat star] \ '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]: diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/HyperNat.thy --- 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 \ '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) diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/NSA.thy --- 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. \r \ Reals. 0 < r --> hnorm x < r}" + "Infinitesimal = {x. \r \ Reals. 0 < r --> hnorm x < r}" definition HFinite :: "('a::real_normed_vector) star set" where - [code del]: "HFinite = {x. \r \ Reals. hnorm x < r}" + "HFinite = {x. \r \ Reals. hnorm x < r}" definition HInfinite :: "('a::real_normed_vector) star set" where - [code del]: "HInfinite = {x. \r \ Reals. r < hnorm x}" + "HInfinite = {x. \r \ 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 \ 'a star \ 'a::real_normed_vector star" where - [transfer_unfold, code del]: "scaleHR = starfun2 scaleR" + [transfer_unfold]: "scaleHR = starfun2 scaleR" lemma Standard_hnorm [simp]: "x \ Standard \ hnorm x \ Standard" by (simp add: hnorm_def) diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/NSCA.thy --- 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 \ HFinite & r:SComplex & r @= x)" + "stc x = (SOME r. x \ HFinite & r:SComplex & r @= x)" subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/NSComplex.thy --- 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 diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/Star.thy --- 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. \As. X = *sn* As}" + "InternalSets = {X. \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 = (\x y. \X \ Rep_star(x). \Y \ Rep_star(y). + "is_starext F f = (\x y. \X \ Rep_star(x). \Y \ 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. \F. X = *fn* F}" + "InternalFuns = {X. \F. X = *fn* F}" (*-------------------------------------------------------- diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/NSA/StarDef.thy --- 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 \ bool" where - [code del]: "unstar b \ b = star_of True" + "unstar b \ b = star_of True" lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \ \)" by (simp add: unstar_def star_of_def star_n_eq_iff) @@ -431,7 +431,7 @@ begin definition - star_zero_def [code del]: "0 \ star_of 0" + star_zero_def: "0 \ star_of 0" instance .. @@ -441,7 +441,7 @@ begin definition - star_one_def [code del]: "1 \ star_of 1" + star_one_def: "1 \ star_of 1" instance .. @@ -451,7 +451,7 @@ begin definition - star_add_def [code del]: "(op +) \ *f2* (op +)" + star_add_def: "(op +) \ *f2* (op +)" instance .. @@ -461,7 +461,7 @@ begin definition - star_mult_def [code del]: "(op *) \ *f2* (op *)" + star_mult_def: "(op *) \ *f2* (op *)" instance .. @@ -471,7 +471,7 @@ begin definition - star_minus_def [code del]: "uminus \ *f* uminus" + star_minus_def: "uminus \ *f* uminus" instance .. @@ -481,7 +481,7 @@ begin definition - star_diff_def [code del]: "(op -) \ *f2* (op -)" + star_diff_def: "(op -) \ *f2* (op -)" instance .. diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Number_Theory/Primes.thy --- 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 \ bool" where - [code del]: "prime_nat p = (1 < p \ (\m. m dvd p --> m = 1 \ m = p))" + "prime_nat p = (1 < p \ (\m. m dvd p --> m = 1 \ m = p))" instance proof qed @@ -58,7 +58,7 @@ definition prime_int :: "int \ bool" where - [code del]: "prime_int p = prime (nat p)" + "prime_int p = prime (nat p)" instance proof qed diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Old_Number_Theory/Legacy_GCD.thy --- 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 \ nat \ nat \ bool" where -- {* @{term gcd} as a relation *} - [code del]: "is_gcd m n p \ p dvd m \ p dvd n \ + "is_gcd m n p \ p dvd m \ p dvd n \ (\d. d dvd m \ d dvd n \ d dvd p)" text {* Uniqueness *} diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Old_Number_Theory/Primes.thy --- 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 \ bool" where - [code del]: "prime p \ (1 < p \ (\m. m dvd p --> m = 1 \ m = p))" + "prime p \ (1 < p \ (\m. m dvd p --> m = 1 \ m = p))" lemma two_is_prime: "prime 2" diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Product_Type.thy --- 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 \ 'c) \ ('b \ 'd) \ 'a \ 'b \ 'c \ 'd" where - [code del]: "prod_fun f g = (\(x, y). (f x, g y))" + "prod_fun f g = (\(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) diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/RealDef.thy --- 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 .. diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/SupInf.thy --- 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. \x\X. x\z)" + Sup_real_def: "Sup X == (LEAST z::real. \