# HG changeset patch # User haftmann # Date 1278924517 -7200 # Node ID a2b7a20d6ea38665d8c04f7cb53a99337f8bf448 # Parent a779f463bae4a52df0ec167f8b42f72053c7a68a dropped superfluous [code del]s diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Complete_Lattice.thy Mon Jul 12 10:48:37 2010 +0200 @@ -193,10 +193,10 @@ begin definition - Inf_fun_def [code del]: "\A = (\x. \{y. \f\A. y = f x})" + Inf_fun_def: "\A = (\x. \{y. \f\A. y = f x})" definition - Sup_fun_def [code del]: "\A = (\x. \{y. \f\A. y = f x})" + Sup_fun_def: "\A = (\x. \{y. \f\A. y = f x})" instance proof qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def @@ -457,7 +457,7 @@ notation (xsymbols) Inter ("\_" [90] 90) -lemma Inter_eq [code del]: +lemma Inter_eq: "\A = {x. \B \ A. x \ B}" proof (rule set_ext) fix x diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Complex.thy Mon Jul 12 10:48:37 2010 +0200 @@ -281,7 +281,7 @@ definition dist_complex_def: "dist x y = cmod (x - y)" -definition open_complex_def [code del]: +definition open_complex_def: "open (S :: complex set) \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" lemmas cmod_def = complex_norm_def diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Divides.thy Mon Jul 12 10:48:37 2010 +0200 @@ -527,7 +527,7 @@ begin definition divmod_nat :: "nat \ nat \ nat \ nat" where - [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)" + "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)" lemma divmod_nat_rel_divmod_nat: "divmod_nat_rel m n (divmod_nat m n)" diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Equiv_Relations.thy Mon Jul 12 10:48:37 2010 +0200 @@ -93,7 +93,7 @@ subsection {* Quotients *} definition quotient :: "'a set \ ('a \ 'a) set \ 'a set set" (infixl "'/'/" 90) where - [code del]: "A//r = (\x \ A. {r``{x}})" -- {* set of equiv classes *} + "A//r = (\x \ A. {r``{x}})" -- {* set of equiv classes *} lemma quotientI: "x \ A ==> r``{x} \ A//r" by (unfold quotient_def) blast diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Finite_Set.thy Mon Jul 12 10:48:37 2010 +0200 @@ -589,7 +589,7 @@ inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x" definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b" where -[code del]: "fold f z A = (THE y. fold_graph f z A y)" + "fold f z A = (THE y. fold_graph f z A y)" text{*A tempting alternative for the definiens is @{term "if finite A then THE y. fold_graph f z A y else e"}. diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Fun.thy Mon Jul 12 10:48:37 2010 +0200 @@ -131,7 +131,7 @@ definition bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective" - [code del]: "bij_betw f A B \ inj_on f A & f ` A = B" + "bij_betw f A B \ inj_on f A & f ` A = B" definition surj :: "('a => 'b) => bool" where diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/FunDef.thy Mon Jul 12 10:48:37 2010 +0200 @@ -224,11 +224,11 @@ subsection {* Concrete orders for SCNP termination proofs *} definition "pair_less = less_than <*lex*> less_than" -definition [code del]: "pair_leq = pair_less^=" +definition "pair_leq = pair_less^=" definition "max_strict = max_ext pair_less" -definition [code del]: "max_weak = max_ext pair_leq \ {({}, {})}" -definition [code del]: "min_strict = min_ext pair_less" -definition [code del]: "min_weak = min_ext pair_leq \ {({}, {})}" +definition "max_weak = max_ext pair_leq \ {({}, {})}" +definition "min_strict = min_ext pair_less" +definition "min_weak = min_ext pair_leq \ {({}, {})}" lemma wf_pair_less[simp]: "wf pair_less" by (auto simp: pair_less_def) diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/HOL.thy Mon Jul 12 10:48:37 2010 +0200 @@ -1138,7 +1138,7 @@ *} definition simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) where - [code del]: "simp_implies \ op ==>" + "simp_implies \ op ==>" lemma simp_impliesI: assumes PQ: "(PROP P \ PROP Q)" diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Int.thy --- a/src/HOL/Int.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Int.thy Mon Jul 12 10:48:37 2010 +0200 @@ -18,7 +18,7 @@ subsection {* The equivalence relation underlying the integers *} definition intrel :: "((nat \ nat) \ (nat \ nat)) set" where - [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }" + "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }" typedef (Integ) int = "UNIV//intrel" @@ -28,34 +28,34 @@ begin definition - Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})" + Zero_int_def: "0 = Abs_Integ (intrel `` {(0, 0)})" definition - One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})" + One_int_def: "1 = Abs_Integ (intrel `` {(1, 0)})" definition - add_int_def [code del]: "z + w = Abs_Integ + add_int_def: "z + w = Abs_Integ (\(x, y) \ Rep_Integ z. \(u, v) \ Rep_Integ w. intrel `` {(x + u, y + v)})" definition - minus_int_def [code del]: + minus_int_def: "- z = Abs_Integ (\(x, y) \ Rep_Integ z. intrel `` {(y, x)})" definition - diff_int_def [code del]: "z - w = z + (-w \ int)" + diff_int_def: "z - w = z + (-w \ int)" definition - mult_int_def [code del]: "z * w = Abs_Integ + mult_int_def: "z * w = Abs_Integ (\(x, y) \ Rep_Integ z. \(u,v ) \ Rep_Integ w. intrel `` {(x*u + y*v, x*v + y*u)})" definition - le_int_def [code del]: + le_int_def: "z \ w \ (\x y u v. x+v \ u+y \ (x, y) \ Rep_Integ z \ (u, v) \ Rep_Integ w)" definition - less_int_def [code del]: "(z\int) < w \ z \ w \ z \ w" + less_int_def: "(z\int) < w \ z \ w \ z \ w" definition zabs_def: "\i\int\ = (if i < 0 then - i else i)" @@ -283,7 +283,7 @@ begin definition of_int :: "int \ 'a" where - [code del]: "of_int z = contents (\(i, j) \ Rep_Integ z. { of_nat i - of_nat j })" + "of_int z = contents (\(i, j) \ Rep_Integ z. { of_nat i - of_nat j })" lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j" proof - @@ -388,10 +388,8 @@ subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *} -definition - nat :: "int \ nat" -where - [code del]: "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" +definition nat :: "int \ nat" where + "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" proof - @@ -593,21 +591,17 @@ subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} -definition - Pls :: int where - [code del]: "Pls = 0" - -definition - Min :: int where - [code del]: "Min = - 1" - -definition - Bit0 :: "int \ int" where - [code del]: "Bit0 k = k + k" - -definition - Bit1 :: "int \ int" where - [code del]: "Bit1 k = 1 + k + k" +definition Pls :: int where + "Pls = 0" + +definition Min :: int where + "Min = - 1" + +definition Bit0 :: "int \ int" where + "Bit0 k = k + k" + +definition Bit1 :: "int \ int" where + "Bit1 k = 1 + k + k" class number = -- {* for numeric types: nat, int, real, \dots *} fixes number_of :: "int \ 'a" @@ -630,13 +624,11 @@ -- {* Unfold all @{text let}s involving constants *} unfolding Let_def .. -definition - succ :: "int \ int" where - [code del]: "succ k = k + 1" - -definition - pred :: "int \ int" where - [code del]: "pred k = k - 1" +definition succ :: "int \ int" where + "succ k = k + 1" + +definition pred :: "int \ int" where + "pred k = k - 1" lemmas max_number_of [simp] = max_def @@ -952,8 +944,8 @@ instantiation int :: number_ring begin -definition int_number_of_def [code del]: - "number_of w = (of_int w \ int)" +definition + int_number_of_def: "number_of w = (of_int w \ int)" instance proof qed (simp only: int_number_of_def) @@ -1274,7 +1266,7 @@ begin definition Ints :: "'a set" where - [code del]: "Ints = range of_int" + "Ints = range of_int" notation (xsymbols) Ints ("\") @@ -2233,7 +2225,8 @@ instantiation int :: eq begin -definition [code del]: "eq_class.eq k l \ k - l = (0\int)" +definition + "eq_class.eq k l \ k - l = (0\int)" instance by default (simp add: eq_int_def) diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Lattices.thy Mon Jul 12 10:48:37 2010 +0200 @@ -623,10 +623,10 @@ begin definition - inf_fun_eq [code del]: "f \ g = (\x. f x \ g x)" + inf_fun_eq: "f \ g = (\x. f x \ g x)" definition - sup_fun_eq [code del]: "f \ g = (\x. f x \ g x)" + sup_fun_eq: "f \ g = (\x. f x \ g x)" instance proof qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq) diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Lim.thy Mon Jul 12 10:48:37 2010 +0200 @@ -23,7 +23,7 @@ definition isUCont :: "['a::metric_space \ 'b::metric_space] \ bool" where - [code del]: "isUCont f = (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" + "isUCont f = (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" subsection {* Limits of Functions *} diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Limits.thy Mon Jul 12 10:48:37 2010 +0200 @@ -37,9 +37,8 @@ subsection {* Eventually *} -definition - eventually :: "('a \ bool) \ 'a net \ bool" where - [code del]: "eventually P net \ Rep_net net P" +definition eventually :: "('a \ bool) \ 'a net \ bool" where + "eventually P net \ Rep_net net P" lemma eventually_Abs_net: assumes "is_filter net" shows "eventually P (Abs_net net) = net P" @@ -114,37 +113,29 @@ begin definition - le_net_def [code del]: - "net \ net' \ (\P. eventually P net' \ eventually P net)" + le_net_def: "net \ net' \ (\P. eventually P net' \ eventually P net)" definition - less_net_def [code del]: - "(net :: 'a net) < net' \ net \ net' \ \ net' \ net" + less_net_def: "(net :: 'a net) < net' \ net \ net' \ \ net' \ net" definition - top_net_def [code del]: - "top = Abs_net (\P. \x. P x)" + top_net_def: "top = Abs_net (\P. \x. P x)" definition - bot_net_def [code del]: - "bot = Abs_net (\P. True)" + bot_net_def: "bot = Abs_net (\P. True)" definition - sup_net_def [code del]: - "sup net net' = Abs_net (\P. eventually P net \ eventually P net')" + sup_net_def: "sup net net' = Abs_net (\P. eventually P net \ eventually P net')" definition - inf_net_def [code del]: - "inf a b = Abs_net + inf_net_def: "inf a b = Abs_net (\P. \Q R. eventually Q a \ eventually R b \ (\x. Q x \ R x \ P x))" definition - Sup_net_def [code del]: - "Sup A = Abs_net (\P. \net\A. eventually P net)" + Sup_net_def: "Sup A = Abs_net (\P. \net\A. eventually P net)" definition - Inf_net_def [code del]: - "Inf A = Sup {x::'a net. \y\A. x \ y}" + Inf_net_def: "Inf A = Sup {x::'a net. \y\A. x \ y}" lemma eventually_top [simp]: "eventually P top \ (\x. P x)" unfolding top_net_def @@ -243,9 +234,7 @@ subsection {* Map function for nets *} -definition - netmap :: "('a \ 'b) \ 'a net \ 'b net" -where [code del]: +definition netmap :: "('a \ 'b) \ 'a net \ 'b net" where "netmap f net = Abs_net (\P. eventually (\x. P (f x)) net)" lemma eventually_netmap: @@ -271,9 +260,7 @@ subsection {* Sequentially *} -definition - sequentially :: "nat net" -where [code del]: +definition sequentially :: "nat net" where "sequentially = Abs_net (\P. \k. \n\k. P n)" lemma eventually_sequentially: @@ -302,19 +289,13 @@ subsection {* Standard Nets *} -definition - within :: "'a net \ 'a set \ 'a net" (infixr "within" 70) -where [code del]: +definition within :: "'a net \ 'a set \ 'a net" (infixr "within" 70) where "net within S = Abs_net (\P. eventually (\x. x \ S \ P x) net)" -definition - nhds :: "'a::topological_space \ 'a net" -where [code del]: +definition nhds :: "'a::topological_space \ 'a net" where "nhds a = Abs_net (\P. \S. open S \ a \ S \ (\x\S. P x))" -definition - at :: "'a::topological_space \ 'a net" -where [code del]: +definition at :: "'a::topological_space \ 'a net" where "at a = nhds a within - {a}" lemma eventually_within: @@ -368,9 +349,8 @@ subsection {* Boundedness *} -definition - Bfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where - [code del]: "Bfun f net = (\K>0. eventually (\x. norm (f x) \ K) net)" +definition Bfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where + "Bfun f net = (\K>0. eventually (\x. norm (f x) \ K) net)" lemma BfunI: assumes K: "eventually (\x. norm (f x) \ K) net" shows "Bfun f net" @@ -390,9 +370,8 @@ subsection {* Convergence to Zero *} -definition - Zfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where - [code del]: "Zfun f net = (\r>0. eventually (\x. norm (f x) < r) net)" +definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where + "Zfun f net = (\r>0. eventually (\x. norm (f x) < r) net)" lemma ZfunI: "(\r. 0 < r \ eventually (\x. norm (f x) < r) net) \ Zfun f net" @@ -547,10 +526,8 @@ subsection {* Limits *} -definition - tendsto :: "('a \ 'b::topological_space) \ 'b \ 'a net \ bool" - (infixr "--->" 55) -where [code del]: +definition tendsto :: "('a \ 'b::topological_space) \ 'b \ 'a net \ bool" + (infixr "--->" 55) where "(f ---> l) net \ (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" ML {* diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/List.thy --- a/src/HOL/List.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/List.thy Mon Jul 12 10:48:37 2010 +0200 @@ -208,7 +208,7 @@ definition list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where - [code del]: "list_all2 P xs ys = + "list_all2 P xs ys = (length xs = length ys \ (\(x, y) \ set (zip xs ys). P x y))" definition @@ -4206,7 +4206,7 @@ definition set_Cons :: "'a set \ 'a list set \ 'a list set" where - [code del]: "set_Cons A XS = {z. \x xs. z = x # xs \ x \ A \ xs \ XS}" + "set_Cons A XS = {z. \x xs. z = x # xs \ x \ A \ xs \ XS}" lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A" by (auto simp add: set_Cons_def) @@ -4229,17 +4229,17 @@ primrec -- {*The lexicographic ordering for lists of the specified length*} lexn :: "('a \ 'a) set \ nat \ ('a list \ 'a list) set" where - [code del]: "lexn r 0 = {}" - | [code del]: "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int + "lexn r 0 = {}" + | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int {(xs, ys). length xs = Suc n \ length ys = Suc n}" definition lex :: "('a \ 'a) set \ ('a list \ 'a list) set" where - [code del]: "lex r = (\n. lexn r n)" -- {*Holds only between lists of the same length*} + "lex r = (\n. lexn r n)" -- {*Holds only between lists of the same length*} definition lenlex :: "('a \ 'a) set => ('a list \ 'a list) set" where - [code del]: "lenlex r = inv_image (less_than <*lex*> lex r) (\xs. (length xs, xs))" + "lenlex r = inv_image (less_than <*lex*> lex r) (\xs. (length xs, xs))" -- {*Compares lists by their length and then lexicographically*} lemma wf_lexn: "wf r ==> wf (lexn r n)" @@ -4313,7 +4313,7 @@ definition lexord :: "('a \ 'a) set \ ('a list \ 'a list) set" where - [code del]: "lexord r = {(x,y ). \ a v. y = x @ a # v \ + "lexord r = {(x,y ). \ a v. y = x @ a # v \ (\ u a b v w. (a,b) \ r \ x = u @ (a # v) \ y = u @ (b # w))}" lemma lexord_Nil_left[simp]: "([],y) \ lexord r = (\ a x. y = a # x)" diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Nat.thy Mon Jul 12 10:48:37 2010 +0200 @@ -48,7 +48,7 @@ instantiation nat :: zero begin -definition Zero_nat_def [code del]: +definition Zero_nat_def: "0 = Abs_Nat Zero_Rep" instance .. @@ -1362,9 +1362,8 @@ context semiring_1 begin -definition - Nats :: "'a set" where - [code del]: "Nats = range of_nat" +definition Nats :: "'a set" where + "Nats = range of_nat" notation (xsymbols) Nats ("\") diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Orderings.thy Mon Jul 12 10:48:37 2010 +0200 @@ -264,10 +264,10 @@ text {* min/max *} definition (in ord) min :: "'a \ 'a \ 'a" where - [code del]: "min a b = (if a \ b then a else b)" + "min a b = (if a \ b then a else b)" definition (in ord) max :: "'a \ 'a \ 'a" where - [code del]: "max a b = (if a \ b then b else a)" + "max a b = (if a \ b then b else a)" lemma min_le_iff_disj: "min x y \ z \ x \ z \ y \ z" @@ -1196,10 +1196,10 @@ begin definition - le_bool_def [code del]: "P \ Q \ P \ Q" + le_bool_def: "P \ Q \ P \ Q" definition - less_bool_def [code del]: "(P\bool) < Q \ \ P \ Q" + less_bool_def: "(P\bool) < Q \ \ P \ Q" definition top_bool_eq: "top = True" @@ -1244,10 +1244,10 @@ begin definition - le_fun_def [code del]: "f \ g \ (\x. f x \ g x)" + le_fun_def: "f \ g \ (\x. f x \ g x)" definition - less_fun_def [code del]: "(f\'a \ 'b) < g \ f \ g \ \ (g \ f)" + less_fun_def: "(f\'a \ 'b) < g \ f \ g \ \ (g \ f)" instance .. diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Predicate.thy Mon Jul 12 10:48:37 2010 +0200 @@ -408,10 +408,10 @@ "P \ Q = Pred (eval P \ eval Q)" definition - [code del]: "\A = Pred (INFI A eval)" + "\A = Pred (INFI A eval)" definition - [code del]: "\A = Pred (SUPR A eval)" + "\A = Pred (SUPR A eval)" definition "- P = Pred (- eval P)" @@ -873,7 +873,7 @@ definition the :: "'a pred => 'a" where - [code del]: "the A = (THE x. eval A x)" + "the A = (THE x. eval A x)" lemma the_eq[code]: "the A = singleton (\x. not_unique A) A" by (auto simp add: the_def singleton_def not_unique_def) diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Quotient_Examples/Quotient_Int.thy --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Jul 12 10:48:37 2010 +0200 @@ -42,7 +42,7 @@ "(uminus \ (int \ int))" is "uminus_int_raw" definition - minus_int_def [code del]: "z - w = z + (-w\int)" + minus_int_def: "z - w = z + (-w\int)" fun times_int_raw :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" @@ -61,7 +61,7 @@ le_int_def: "(op \) :: int \ int \ bool" is "le_int_raw" definition - less_int_def [code del]: "(z\int) < w = (z \ w \ z \ w)" + less_int_def: "(z\int) < w = (z \ w \ z \ w)" definition zabs_def: "\i\int\ = (if i < 0 then - i else i)" diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/RealDef.thy Mon Jul 12 10:48:37 2010 +0200 @@ -751,7 +751,7 @@ begin definition - [code del]: "(number_of x :: real) = of_int x" + "(number_of x :: real) = of_int x" instance proof qed (rule number_of_real_def) diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/RealVector.thy --- a/src/HOL/RealVector.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/RealVector.thy Mon Jul 12 10:48:37 2010 +0200 @@ -305,9 +305,8 @@ subsection {* The Set of Real Numbers *} -definition - Reals :: "'a::real_algebra_1 set" where - [code del]: "Reals = range of_real" +definition Reals :: "'a::real_algebra_1 set" where + "Reals = range of_real" notation (xsymbols) Reals ("\") @@ -786,7 +785,7 @@ definition dist_real_def: "dist x y = \x - y\" -definition open_real_def [code del]: +definition open_real_def: "open (S :: real set) \ (\