--- 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]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+ Inf_fun_def: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
definition
- Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+ Sup_fun_def: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>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 ("\<Inter>_" [90] 90)
-lemma Inter_eq [code del]:
+lemma Inter_eq:
"\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
proof (rule set_ext)
fix x
--- 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) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
lemmas cmod_def = complex_norm_def
--- 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 \<Rightarrow> nat \<Rightarrow> nat \<times> 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)"
--- 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 \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where
- [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
+ "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
by (unfold quotient_def) blast
--- 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 \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> '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"}.
--- 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 \<longleftrightarrow> inj_on f A & f ` A = B"
+ "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
definition
surj :: "('a => 'b) => bool" where
--- 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 \<union> {({}, {})}"
-definition [code del]: "min_strict = min_ext pair_less"
-definition [code del]: "min_weak = min_ext pair_leq \<union> {({}, {})}"
+definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
+definition "min_strict = min_ext pair_less"
+definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
lemma wf_pair_less[simp]: "wf pair_less"
by (auto simp: pair_less_def)
--- 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 \<equiv> op ==>"
+ "simp_implies \<equiv> op ==>"
lemma simp_impliesI:
assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
--- 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 \<times> nat) \<times> (nat \<times> 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
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
intrel `` {(x + u, y + v)})"
definition
- minus_int_def [code del]:
+ minus_int_def:
"- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
definition
- diff_int_def [code del]: "z - w = z + (-w \<Colon> int)"
+ diff_int_def: "z - w = z + (-w \<Colon> int)"
definition
- mult_int_def [code del]: "z * w = Abs_Integ
+ mult_int_def: "z * w = Abs_Integ
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
intrel `` {(x*u + y*v, x*v + y*u)})"
definition
- le_int_def [code del]:
+ le_int_def:
"z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
definition
- less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+ less_int_def: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
definition
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
@@ -283,7 +283,7 @@
begin
definition of_int :: "int \<Rightarrow> 'a" where
- [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+ "of_int z = contents (\<Union>(i, j) \<in> 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 \<Rightarrow> nat"
-where
- [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
+definition nat :: "int \<Rightarrow> nat" where
+ "nat z = contents (\<Union>(x, y) \<in> 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 \<Rightarrow> int" where
- [code del]: "Bit0 k = k + k"
-
-definition
- Bit1 :: "int \<Rightarrow> int" where
- [code del]: "Bit1 k = 1 + k + k"
+definition Pls :: int where
+ "Pls = 0"
+
+definition Min :: int where
+ "Min = - 1"
+
+definition Bit0 :: "int \<Rightarrow> int" where
+ "Bit0 k = k + k"
+
+definition Bit1 :: "int \<Rightarrow> int" where
+ "Bit1 k = 1 + k + k"
class number = -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
@@ -630,13 +624,11 @@
-- {* Unfold all @{text let}s involving constants *}
unfolding Let_def ..
-definition
- succ :: "int \<Rightarrow> int" where
- [code del]: "succ k = k + 1"
-
-definition
- pred :: "int \<Rightarrow> int" where
- [code del]: "pred k = k - 1"
+definition succ :: "int \<Rightarrow> int" where
+ "succ k = k + 1"
+
+definition pred :: "int \<Rightarrow> 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 \<Colon> int)"
+definition
+ int_number_of_def: "number_of w = (of_int w \<Colon> 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 ("\<int>")
@@ -2233,7 +2225,8 @@
instantiation int :: eq
begin
-definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+definition
+ "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
instance by default (simp add: eq_int_def)
--- 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 \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+ inf_fun_eq: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
definition
- sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+ sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
instance proof
qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)
--- 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 \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
- [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
+ "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
subsection {* Limits of Functions *}
--- 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 \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "eventually P net \<longleftrightarrow> Rep_net net P"
+definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
+ "eventually P net \<longleftrightarrow> 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 \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
+ le_net_def: "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
definition
- less_net_def [code del]:
- "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
+ less_net_def: "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
definition
- top_net_def [code del]:
- "top = Abs_net (\<lambda>P. \<forall>x. P x)"
+ top_net_def: "top = Abs_net (\<lambda>P. \<forall>x. P x)"
definition
- bot_net_def [code del]:
- "bot = Abs_net (\<lambda>P. True)"
+ bot_net_def: "bot = Abs_net (\<lambda>P. True)"
definition
- sup_net_def [code del]:
- "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
+ sup_net_def: "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
definition
- inf_net_def [code del]:
- "inf a b = Abs_net
+ inf_net_def: "inf a b = Abs_net
(\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
definition
- Sup_net_def [code del]:
- "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
+ Sup_net_def: "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
definition
- Inf_net_def [code del]:
- "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
+ Inf_net_def: "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
unfolding top_net_def
@@ -243,9 +234,7 @@
subsection {* Map function for nets *}
-definition
- netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net"
-where [code del]:
+definition netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net" where
"netmap f net = Abs_net (\<lambda>P. eventually (\<lambda>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 (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
lemma eventually_sequentially:
@@ -302,19 +289,13 @@
subsection {* Standard Nets *}
-definition
- within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
-where [code del]:
+definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
"net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
-definition
- nhds :: "'a::topological_space \<Rightarrow> 'a net"
-where [code del]:
+definition nhds :: "'a::topological_space \<Rightarrow> 'a net" where
"nhds a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
-definition
- at :: "'a::topological_space \<Rightarrow> 'a net"
-where [code del]:
+definition at :: "'a::topological_space \<Rightarrow> 'a net" where
"at a = nhds a within - {a}"
lemma eventually_within:
@@ -368,9 +349,8 @@
subsection {* Boundedness *}
-definition
- Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
+definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
+ "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
lemma BfunI:
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net"
@@ -390,9 +370,8 @@
subsection {* Convergence to Zero *}
-definition
- Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
+definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
+ "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
lemma ZfunI:
"(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net"
@@ -547,10 +526,8 @@
subsection {* Limits *}
-definition
- tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
- (infixr "--->" 55)
-where [code del]:
+definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
+ (infixr "--->" 55) where
"(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
ML {*
--- 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 \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
definition
@@ -4206,7 +4206,7 @@
definition
set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
- [code del]: "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
+ "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> 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 \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> '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 \<and> length ys = Suc n}"
definition
lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
- [code del]: "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
+ "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
definition
lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
- [code del]: "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
+ "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>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 \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
- [code del]: "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
+ "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
(\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
--- 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 ("\<nat>")
--- 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 \<Rightarrow> 'a \<Rightarrow> 'a" where
- [code del]: "min a b = (if a \<le> b then a else b)"
+ "min a b = (if a \<le> b then a else b)"
definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- [code del]: "max a b = (if a \<le> b then b else a)"
+ "max a b = (if a \<le> b then b else a)"
lemma min_le_iff_disj:
"min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
@@ -1196,10 +1196,10 @@
begin
definition
- le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
+ le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
definition
- less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
+ less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
definition
top_bool_eq: "top = True"
@@ -1244,10 +1244,10 @@
begin
definition
- le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
+ le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
definition
- less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
+ less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
instance ..
--- 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 \<squnion> Q = Pred (eval P \<squnion> eval Q)"
definition
- [code del]: "\<Sqinter>A = Pred (INFI A eval)"
+ "\<Sqinter>A = Pred (INFI A eval)"
definition
- [code del]: "\<Squnion>A = Pred (SUPR A eval)"
+ "\<Squnion>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 (\<lambda>x. not_unique A) A"
by (auto simp add: the_def singleton_def not_unique_def)
--- 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 \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
definition
- minus_int_def [code del]: "z - w = z + (-w\<Colon>int)"
+ minus_int_def: "z - w = z + (-w\<Colon>int)"
fun
times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -61,7 +61,7 @@
le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
definition
- less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+ less_int_def: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
definition
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
--- 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)
--- 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 ("\<real>")
@@ -786,7 +785,7 @@
definition dist_real_def:
"dist x y = \<bar>x - y\<bar>"
-definition open_real_def [code del]:
+definition open_real_def:
"open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
instance
--- a/src/HOL/Recdef.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Recdef.thy Mon Jul 12 10:48:37 2010 +0200
@@ -38,7 +38,7 @@
definition
wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
- [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+ "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
subsection{*Well-Founded Recursion*}
--- a/src/HOL/Rings.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Rings.thy Mon Jul 12 10:48:37 2010 +0200
@@ -96,7 +96,7 @@
begin
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
- [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
+ "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
unfolding dvd_def ..
--- a/src/HOL/SEQ.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/SEQ.thy Mon Jul 12 10:48:37 2010 +0200
@@ -31,7 +31,7 @@
definition
Bseq :: "(nat => 'a::real_normed_vector) => bool" where
--{*Standard definition for bounded sequence*}
- [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
+ "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
definition
monoseq :: "(nat=>real)=>bool" where
@@ -39,27 +39,27 @@
The use of disjunction here complicates proofs considerably.
One alternative is to add a Boolean argument to indicate the direction.
Another is to develop the notions of increasing and decreasing first.*}
- [code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
+ "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
definition
incseq :: "(nat=>real)=>bool" where
--{*Increasing sequence*}
- [code del]: "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
+ "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
definition
decseq :: "(nat=>real)=>bool" where
--{*Increasing sequence*}
- [code del]: "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+ "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
definition
subseq :: "(nat => nat) => bool" where
--{*Definition of subsequence*}
- [code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
+ "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
definition
Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
--{*Standard definition of the Cauchy condition*}
- [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
+ "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
subsection {* Bounded Sequences *}
--- a/src/HOL/Set.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Set.thy Mon Jul 12 10:48:37 2010 +0200
@@ -1574,7 +1574,7 @@
subsubsection {* Inverse image of a function *}
definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where
- [code del]: "f -` B == {x. f x : B}"
+ "f -` B == {x. f x : B}"
lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
by (unfold vimage_def) blast
@@ -1657,7 +1657,7 @@
subsubsection {* Getting the Contents of a Singleton Set *}
definition contents :: "'a set \<Rightarrow> 'a" where
- [code del]: "contents X = (THE x. X = {x})"
+ "contents X = (THE x. X = {x})"
lemma contents_eq [simp]: "contents {x} = x"
by (simp add: contents_def)
--- a/src/HOL/Wellfounded.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Wellfounded.thy Mon Jul 12 10:48:37 2010 +0200
@@ -682,9 +682,8 @@
text{* Lexicographic combinations *}
-definition
- lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
- [code del]: "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
+definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
+ "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
apply (unfold wf_def lex_prod_def)
@@ -819,10 +818,8 @@
by (force elim!: max_ext.cases)
-definition
- min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
-where
- [code del]: "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
+definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" where
+ "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
lemma min_ext_wf:
assumes "wf r"