dropped superfluous [code del]s
authorhaftmann
Mon Jul 12 10:48:37 2010 +0200 (2010-07-12)
changeset 37767a2b7a20d6ea3
parent 37766 a779f463bae4
child 37769 4511931c0692
dropped superfluous [code del]s
src/HOL/Complete_Lattice.thy
src/HOL/Complex.thy
src/HOL/Divides.thy
src/HOL/Equiv_Relations.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/FunDef.thy
src/HOL/HOL.thy
src/HOL/Int.thy
src/HOL/Lattices.thy
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Predicate.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/RealDef.thy
src/HOL/RealVector.thy
src/HOL/Recdef.thy
src/HOL/Rings.thy
src/HOL/SEQ.thy
src/HOL/Set.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -193,10 +193,10 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
     1.8 +  Inf_fun_def: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
     1.9  
    1.10  definition
    1.11 -  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
    1.12 +  Sup_fun_def: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
    1.13  
    1.14  instance proof
    1.15  qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
    1.16 @@ -457,7 +457,7 @@
    1.17  notation (xsymbols)
    1.18    Inter  ("\<Inter>_" [90] 90)
    1.19  
    1.20 -lemma Inter_eq [code del]:
    1.21 +lemma Inter_eq:
    1.22    "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
    1.23  proof (rule set_ext)
    1.24    fix x
     2.1 --- a/src/HOL/Complex.thy	Mon Jul 12 08:58:27 2010 +0200
     2.2 +++ b/src/HOL/Complex.thy	Mon Jul 12 10:48:37 2010 +0200
     2.3 @@ -281,7 +281,7 @@
     2.4  definition dist_complex_def:
     2.5    "dist x y = cmod (x - y)"
     2.6  
     2.7 -definition open_complex_def [code del]:
     2.8 +definition open_complex_def:
     2.9    "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    2.10  
    2.11  lemmas cmod_def = complex_norm_def
     3.1 --- a/src/HOL/Divides.thy	Mon Jul 12 08:58:27 2010 +0200
     3.2 +++ b/src/HOL/Divides.thy	Mon Jul 12 10:48:37 2010 +0200
     3.3 @@ -527,7 +527,7 @@
     3.4  begin
     3.5  
     3.6  definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
     3.7 -  [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
     3.8 +  "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
     3.9  
    3.10  lemma divmod_nat_rel_divmod_nat:
    3.11    "divmod_nat_rel m n (divmod_nat m n)"
     4.1 --- a/src/HOL/Equiv_Relations.thy	Mon Jul 12 08:58:27 2010 +0200
     4.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Jul 12 10:48:37 2010 +0200
     4.3 @@ -93,7 +93,7 @@
     4.4  subsection {* Quotients *}
     4.5  
     4.6  definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"  (infixl "'/'/" 90) where
     4.7 -  [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
     4.8 +  "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
     4.9  
    4.10  lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
    4.11    by (unfold quotient_def) blast
     5.1 --- a/src/HOL/Finite_Set.thy	Mon Jul 12 08:58:27 2010 +0200
     5.2 +++ b/src/HOL/Finite_Set.thy	Mon Jul 12 10:48:37 2010 +0200
     5.3 @@ -589,7 +589,7 @@
     5.4  inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
     5.5  
     5.6  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where
     5.7 -[code del]: "fold f z A = (THE y. fold_graph f z A y)"
     5.8 +  "fold f z A = (THE y. fold_graph f z A y)"
     5.9  
    5.10  text{*A tempting alternative for the definiens is
    5.11  @{term "if finite A then THE y. fold_graph f z A y else e"}.
     6.1 --- a/src/HOL/Fun.thy	Mon Jul 12 08:58:27 2010 +0200
     6.2 +++ b/src/HOL/Fun.thy	Mon Jul 12 10:48:37 2010 +0200
     6.3 @@ -131,7 +131,7 @@
     6.4  
     6.5  definition
     6.6    bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
     6.7 -  [code del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
     6.8 +  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
     6.9  
    6.10  definition
    6.11    surj :: "('a => 'b) => bool" where
     7.1 --- a/src/HOL/FunDef.thy	Mon Jul 12 08:58:27 2010 +0200
     7.2 +++ b/src/HOL/FunDef.thy	Mon Jul 12 10:48:37 2010 +0200
     7.3 @@ -224,11 +224,11 @@
     7.4  subsection {* Concrete orders for SCNP termination proofs *}
     7.5  
     7.6  definition "pair_less = less_than <*lex*> less_than"
     7.7 -definition [code del]: "pair_leq = pair_less^="
     7.8 +definition "pair_leq = pair_less^="
     7.9  definition "max_strict = max_ext pair_less"
    7.10 -definition [code del]: "max_weak = max_ext pair_leq \<union> {({}, {})}"
    7.11 -definition [code del]: "min_strict = min_ext pair_less"
    7.12 -definition [code del]: "min_weak = min_ext pair_leq \<union> {({}, {})}"
    7.13 +definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
    7.14 +definition "min_strict = min_ext pair_less"
    7.15 +definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
    7.16  
    7.17  lemma wf_pair_less[simp]: "wf pair_less"
    7.18    by (auto simp: pair_less_def)
     8.1 --- a/src/HOL/HOL.thy	Mon Jul 12 08:58:27 2010 +0200
     8.2 +++ b/src/HOL/HOL.thy	Mon Jul 12 10:48:37 2010 +0200
     8.3 @@ -1138,7 +1138,7 @@
     8.4  *}
     8.5  
     8.6  definition simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1) where
     8.7 -  [code del]: "simp_implies \<equiv> op ==>"
     8.8 +  "simp_implies \<equiv> op ==>"
     8.9  
    8.10  lemma simp_impliesI:
    8.11    assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
     9.1 --- a/src/HOL/Int.thy	Mon Jul 12 08:58:27 2010 +0200
     9.2 +++ b/src/HOL/Int.thy	Mon Jul 12 10:48:37 2010 +0200
     9.3 @@ -18,7 +18,7 @@
     9.4  subsection {* The equivalence relation underlying the integers *}
     9.5  
     9.6  definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
     9.7 -  [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
     9.8 +  "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
     9.9  
    9.10  typedef (Integ)
    9.11    int = "UNIV//intrel"
    9.12 @@ -28,34 +28,34 @@
    9.13  begin
    9.14  
    9.15  definition
    9.16 -  Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
    9.17 +  Zero_int_def: "0 = Abs_Integ (intrel `` {(0, 0)})"
    9.18  
    9.19  definition
    9.20 -  One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
    9.21 +  One_int_def: "1 = Abs_Integ (intrel `` {(1, 0)})"
    9.22  
    9.23  definition
    9.24 -  add_int_def [code del]: "z + w = Abs_Integ
    9.25 +  add_int_def: "z + w = Abs_Integ
    9.26      (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    9.27        intrel `` {(x + u, y + v)})"
    9.28  
    9.29  definition
    9.30 -  minus_int_def [code del]:
    9.31 +  minus_int_def:
    9.32      "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    9.33  
    9.34  definition
    9.35 -  diff_int_def [code del]:  "z - w = z + (-w \<Colon> int)"
    9.36 +  diff_int_def:  "z - w = z + (-w \<Colon> int)"
    9.37  
    9.38  definition
    9.39 -  mult_int_def [code del]: "z * w = Abs_Integ
    9.40 +  mult_int_def: "z * w = Abs_Integ
    9.41      (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
    9.42        intrel `` {(x*u + y*v, x*v + y*u)})"
    9.43  
    9.44  definition
    9.45 -  le_int_def [code del]:
    9.46 +  le_int_def:
    9.47     "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)"
    9.48  
    9.49  definition
    9.50 -  less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
    9.51 +  less_int_def: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
    9.52  
    9.53  definition
    9.54    zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    9.55 @@ -283,7 +283,7 @@
    9.56  begin
    9.57  
    9.58  definition of_int :: "int \<Rightarrow> 'a" where
    9.59 -  [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    9.60 +  "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    9.61  
    9.62  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
    9.63  proof -
    9.64 @@ -388,10 +388,8 @@
    9.65  
    9.66  subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
    9.67  
    9.68 -definition
    9.69 -  nat :: "int \<Rightarrow> nat"
    9.70 -where
    9.71 -  [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
    9.72 +definition nat :: "int \<Rightarrow> nat" where
    9.73 +  "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
    9.74  
    9.75  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
    9.76  proof -
    9.77 @@ -593,21 +591,17 @@
    9.78  
    9.79  subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
    9.80  
    9.81 -definition
    9.82 -  Pls :: int where
    9.83 -  [code del]: "Pls = 0"
    9.84 -
    9.85 -definition
    9.86 -  Min :: int where
    9.87 -  [code del]: "Min = - 1"
    9.88 -
    9.89 -definition
    9.90 -  Bit0 :: "int \<Rightarrow> int" where
    9.91 -  [code del]: "Bit0 k = k + k"
    9.92 -
    9.93 -definition
    9.94 -  Bit1 :: "int \<Rightarrow> int" where
    9.95 -  [code del]: "Bit1 k = 1 + k + k"
    9.96 +definition Pls :: int where
    9.97 +  "Pls = 0"
    9.98 +
    9.99 +definition Min :: int where
   9.100 +  "Min = - 1"
   9.101 +
   9.102 +definition Bit0 :: "int \<Rightarrow> int" where
   9.103 +  "Bit0 k = k + k"
   9.104 +
   9.105 +definition Bit1 :: "int \<Rightarrow> int" where
   9.106 +  "Bit1 k = 1 + k + k"
   9.107  
   9.108  class number = -- {* for numeric types: nat, int, real, \dots *}
   9.109    fixes number_of :: "int \<Rightarrow> 'a"
   9.110 @@ -630,13 +624,11 @@
   9.111    -- {* Unfold all @{text let}s involving constants *}
   9.112    unfolding Let_def ..
   9.113  
   9.114 -definition
   9.115 -  succ :: "int \<Rightarrow> int" where
   9.116 -  [code del]: "succ k = k + 1"
   9.117 -
   9.118 -definition
   9.119 -  pred :: "int \<Rightarrow> int" where
   9.120 -  [code del]: "pred k = k - 1"
   9.121 +definition succ :: "int \<Rightarrow> int" where
   9.122 +  "succ k = k + 1"
   9.123 +
   9.124 +definition pred :: "int \<Rightarrow> int" where
   9.125 +  "pred k = k - 1"
   9.126  
   9.127  lemmas
   9.128    max_number_of [simp] = max_def
   9.129 @@ -952,8 +944,8 @@
   9.130  instantiation int :: number_ring
   9.131  begin
   9.132  
   9.133 -definition int_number_of_def [code del]:
   9.134 -  "number_of w = (of_int w \<Colon> int)"
   9.135 +definition
   9.136 +  int_number_of_def: "number_of w = (of_int w \<Colon> int)"
   9.137  
   9.138  instance proof
   9.139  qed (simp only: int_number_of_def)
   9.140 @@ -1274,7 +1266,7 @@
   9.141  begin
   9.142  
   9.143  definition Ints  :: "'a set" where
   9.144 -  [code del]: "Ints = range of_int"
   9.145 +  "Ints = range of_int"
   9.146  
   9.147  notation (xsymbols)
   9.148    Ints  ("\<int>")
   9.149 @@ -2233,7 +2225,8 @@
   9.150  instantiation int :: eq
   9.151  begin
   9.152  
   9.153 -definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
   9.154 +definition
   9.155 +  "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
   9.156  
   9.157  instance by default (simp add: eq_int_def)
   9.158  
    10.1 --- a/src/HOL/Lattices.thy	Mon Jul 12 08:58:27 2010 +0200
    10.2 +++ b/src/HOL/Lattices.thy	Mon Jul 12 10:48:37 2010 +0200
    10.3 @@ -623,10 +623,10 @@
    10.4  begin
    10.5  
    10.6  definition
    10.7 -  inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    10.8 +  inf_fun_eq: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    10.9  
   10.10  definition
   10.11 -  sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   10.12 +  sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   10.13  
   10.14  instance proof
   10.15  qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)
    11.1 --- a/src/HOL/Lim.thy	Mon Jul 12 08:58:27 2010 +0200
    11.2 +++ b/src/HOL/Lim.thy	Mon Jul 12 10:48:37 2010 +0200
    11.3 @@ -23,7 +23,7 @@
    11.4  
    11.5  definition
    11.6    isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
    11.7 -  [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
    11.8 +  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
    11.9  
   11.10  subsection {* Limits of Functions *}
   11.11  
    12.1 --- a/src/HOL/Limits.thy	Mon Jul 12 08:58:27 2010 +0200
    12.2 +++ b/src/HOL/Limits.thy	Mon Jul 12 10:48:37 2010 +0200
    12.3 @@ -37,9 +37,8 @@
    12.4  
    12.5  subsection {* Eventually *}
    12.6  
    12.7 -definition
    12.8 -  eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
    12.9 -  [code del]: "eventually P net \<longleftrightarrow> Rep_net net P"
   12.10 +definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
   12.11 +  "eventually P net \<longleftrightarrow> Rep_net net P"
   12.12  
   12.13  lemma eventually_Abs_net:
   12.14    assumes "is_filter net" shows "eventually P (Abs_net net) = net P"
   12.15 @@ -114,37 +113,29 @@
   12.16  begin
   12.17  
   12.18  definition
   12.19 -  le_net_def [code del]:
   12.20 -    "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
   12.21 +  le_net_def: "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
   12.22  
   12.23  definition
   12.24 -  less_net_def [code del]:
   12.25 -    "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
   12.26 +  less_net_def: "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
   12.27  
   12.28  definition
   12.29 -  top_net_def [code del]:
   12.30 -    "top = Abs_net (\<lambda>P. \<forall>x. P x)"
   12.31 +  top_net_def: "top = Abs_net (\<lambda>P. \<forall>x. P x)"
   12.32  
   12.33  definition
   12.34 -  bot_net_def [code del]:
   12.35 -    "bot = Abs_net (\<lambda>P. True)"
   12.36 +  bot_net_def: "bot = Abs_net (\<lambda>P. True)"
   12.37  
   12.38  definition
   12.39 -  sup_net_def [code del]:
   12.40 -    "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
   12.41 +  sup_net_def: "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
   12.42  
   12.43  definition
   12.44 -  inf_net_def [code del]:
   12.45 -    "inf a b = Abs_net
   12.46 +  inf_net_def: "inf a b = Abs_net
   12.47        (\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   12.48  
   12.49  definition
   12.50 -  Sup_net_def [code del]:
   12.51 -    "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
   12.52 +  Sup_net_def: "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
   12.53  
   12.54  definition
   12.55 -  Inf_net_def [code del]:
   12.56 -    "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
   12.57 +  Inf_net_def: "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
   12.58  
   12.59  lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
   12.60  unfolding top_net_def
   12.61 @@ -243,9 +234,7 @@
   12.62  
   12.63  subsection {* Map function for nets *}
   12.64  
   12.65 -definition
   12.66 -  netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net"
   12.67 -where [code del]:
   12.68 +definition netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net" where
   12.69    "netmap f net = Abs_net (\<lambda>P. eventually (\<lambda>x. P (f x)) net)"
   12.70  
   12.71  lemma eventually_netmap:
   12.72 @@ -271,9 +260,7 @@
   12.73  
   12.74  subsection {* Sequentially *}
   12.75  
   12.76 -definition
   12.77 -  sequentially :: "nat net"
   12.78 -where [code del]:
   12.79 +definition sequentially :: "nat net" where
   12.80    "sequentially = Abs_net (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
   12.81  
   12.82  lemma eventually_sequentially:
   12.83 @@ -302,19 +289,13 @@
   12.84  
   12.85  subsection {* Standard Nets *}
   12.86  
   12.87 -definition
   12.88 -  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
   12.89 -where [code del]:
   12.90 +definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
   12.91    "net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
   12.92  
   12.93 -definition
   12.94 -  nhds :: "'a::topological_space \<Rightarrow> 'a net"
   12.95 -where [code del]:
   12.96 +definition nhds :: "'a::topological_space \<Rightarrow> 'a net" where
   12.97    "nhds a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   12.98  
   12.99 -definition
  12.100 -  at :: "'a::topological_space \<Rightarrow> 'a net"
  12.101 -where [code del]:
  12.102 +definition at :: "'a::topological_space \<Rightarrow> 'a net" where
  12.103    "at a = nhds a within - {a}"
  12.104  
  12.105  lemma eventually_within:
  12.106 @@ -368,9 +349,8 @@
  12.107  
  12.108  subsection {* Boundedness *}
  12.109  
  12.110 -definition
  12.111 -  Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
  12.112 -  [code del]: "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
  12.113 +definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
  12.114 +  "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
  12.115  
  12.116  lemma BfunI:
  12.117    assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net"
  12.118 @@ -390,9 +370,8 @@
  12.119  
  12.120  subsection {* Convergence to Zero *}
  12.121  
  12.122 -definition
  12.123 -  Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
  12.124 -  [code del]: "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
  12.125 +definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
  12.126 +  "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
  12.127  
  12.128  lemma ZfunI:
  12.129    "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net"
  12.130 @@ -547,10 +526,8 @@
  12.131  
  12.132  subsection {* Limits *}
  12.133  
  12.134 -definition
  12.135 -  tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
  12.136 -    (infixr "--->" 55)
  12.137 -where [code del]:
  12.138 +definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
  12.139 +    (infixr "--->" 55) where
  12.140    "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
  12.141  
  12.142  ML {*
    13.1 --- a/src/HOL/List.thy	Mon Jul 12 08:58:27 2010 +0200
    13.2 +++ b/src/HOL/List.thy	Mon Jul 12 10:48:37 2010 +0200
    13.3 @@ -208,7 +208,7 @@
    13.4  
    13.5  definition
    13.6    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
    13.7 -  [code del]: "list_all2 P xs ys =
    13.8 +  "list_all2 P xs ys =
    13.9      (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
   13.10  
   13.11  definition
   13.12 @@ -4206,7 +4206,7 @@
   13.13  
   13.14  definition
   13.15    set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
   13.16 -  [code del]: "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
   13.17 +  "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
   13.18  
   13.19  lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
   13.20  by (auto simp add: set_Cons_def)
   13.21 @@ -4229,17 +4229,17 @@
   13.22          
   13.23  primrec -- {*The lexicographic ordering for lists of the specified length*}
   13.24    lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
   13.25 -    [code del]: "lexn r 0 = {}"
   13.26 -  | [code del]: "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
   13.27 +    "lexn r 0 = {}"
   13.28 +  | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
   13.29        {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
   13.30  
   13.31  definition
   13.32    lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   13.33 -  [code del]: "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
   13.34 +  "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
   13.35  
   13.36  definition
   13.37    lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
   13.38 -  [code del]: "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
   13.39 +  "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
   13.40          -- {*Compares lists by their length and then lexicographically*}
   13.41  
   13.42  lemma wf_lexn: "wf r ==> wf (lexn r n)"
   13.43 @@ -4313,7 +4313,7 @@
   13.44  
   13.45  definition
   13.46    lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   13.47 -  [code del]: "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
   13.48 +  "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
   13.49              (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
   13.50  
   13.51  lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
    14.1 --- a/src/HOL/Nat.thy	Mon Jul 12 08:58:27 2010 +0200
    14.2 +++ b/src/HOL/Nat.thy	Mon Jul 12 10:48:37 2010 +0200
    14.3 @@ -48,7 +48,7 @@
    14.4  instantiation nat :: zero
    14.5  begin
    14.6  
    14.7 -definition Zero_nat_def [code del]:
    14.8 +definition Zero_nat_def:
    14.9    "0 = Abs_Nat Zero_Rep"
   14.10  
   14.11  instance ..
   14.12 @@ -1362,9 +1362,8 @@
   14.13  context semiring_1
   14.14  begin
   14.15  
   14.16 -definition
   14.17 -  Nats  :: "'a set" where
   14.18 -  [code del]: "Nats = range of_nat"
   14.19 +definition Nats  :: "'a set" where
   14.20 +  "Nats = range of_nat"
   14.21  
   14.22  notation (xsymbols)
   14.23    Nats  ("\<nat>")
    15.1 --- a/src/HOL/Orderings.thy	Mon Jul 12 08:58:27 2010 +0200
    15.2 +++ b/src/HOL/Orderings.thy	Mon Jul 12 10:48:37 2010 +0200
    15.3 @@ -264,10 +264,10 @@
    15.4  text {* min/max *}
    15.5  
    15.6  definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    15.7 -  [code del]: "min a b = (if a \<le> b then a else b)"
    15.8 +  "min a b = (if a \<le> b then a else b)"
    15.9  
   15.10  definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   15.11 -  [code del]: "max a b = (if a \<le> b then b else a)"
   15.12 +  "max a b = (if a \<le> b then b else a)"
   15.13  
   15.14  lemma min_le_iff_disj:
   15.15    "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
   15.16 @@ -1196,10 +1196,10 @@
   15.17  begin
   15.18  
   15.19  definition
   15.20 -  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
   15.21 +  le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
   15.22  
   15.23  definition
   15.24 -  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
   15.25 +  less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
   15.26  
   15.27  definition
   15.28    top_bool_eq: "top = True"
   15.29 @@ -1244,10 +1244,10 @@
   15.30  begin
   15.31  
   15.32  definition
   15.33 -  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
   15.34 +  le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
   15.35  
   15.36  definition
   15.37 -  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
   15.38 +  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
   15.39  
   15.40  instance ..
   15.41  
    16.1 --- a/src/HOL/Predicate.thy	Mon Jul 12 08:58:27 2010 +0200
    16.2 +++ b/src/HOL/Predicate.thy	Mon Jul 12 10:48:37 2010 +0200
    16.3 @@ -408,10 +408,10 @@
    16.4    "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
    16.5  
    16.6  definition
    16.7 -  [code del]: "\<Sqinter>A = Pred (INFI A eval)"
    16.8 +  "\<Sqinter>A = Pred (INFI A eval)"
    16.9  
   16.10  definition
   16.11 -  [code del]: "\<Squnion>A = Pred (SUPR A eval)"
   16.12 +  "\<Squnion>A = Pred (SUPR A eval)"
   16.13  
   16.14  definition
   16.15    "- P = Pred (- eval P)"
   16.16 @@ -873,7 +873,7 @@
   16.17  
   16.18  definition the :: "'a pred => 'a"
   16.19  where
   16.20 -  [code del]: "the A = (THE x. eval A x)"
   16.21 +  "the A = (THE x. eval A x)"
   16.22  
   16.23  lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A"
   16.24  by (auto simp add: the_def singleton_def not_unique_def)
    17.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Jul 12 08:58:27 2010 +0200
    17.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Jul 12 10:48:37 2010 +0200
    17.3 @@ -42,7 +42,7 @@
    17.4    "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
    17.5  
    17.6  definition
    17.7 -  minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"
    17.8 +  minus_int_def:  "z - w = z + (-w\<Colon>int)"
    17.9  
   17.10  fun
   17.11    times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
   17.12 @@ -61,7 +61,7 @@
   17.13    le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
   17.14  
   17.15  definition
   17.16 -  less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
   17.17 +  less_int_def: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
   17.18  
   17.19  definition
   17.20    zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    18.1 --- a/src/HOL/RealDef.thy	Mon Jul 12 08:58:27 2010 +0200
    18.2 +++ b/src/HOL/RealDef.thy	Mon Jul 12 10:48:37 2010 +0200
    18.3 @@ -751,7 +751,7 @@
    18.4  begin
    18.5  
    18.6  definition
    18.7 -  [code del]: "(number_of x :: real) = of_int x"
    18.8 +  "(number_of x :: real) = of_int x"
    18.9  
   18.10  instance proof
   18.11  qed (rule number_of_real_def)
    19.1 --- a/src/HOL/RealVector.thy	Mon Jul 12 08:58:27 2010 +0200
    19.2 +++ b/src/HOL/RealVector.thy	Mon Jul 12 10:48:37 2010 +0200
    19.3 @@ -305,9 +305,8 @@
    19.4  
    19.5  subsection {* The Set of Real Numbers *}
    19.6  
    19.7 -definition
    19.8 -  Reals :: "'a::real_algebra_1 set" where
    19.9 -  [code del]: "Reals = range of_real"
   19.10 +definition Reals :: "'a::real_algebra_1 set" where
   19.11 +  "Reals = range of_real"
   19.12  
   19.13  notation (xsymbols)
   19.14    Reals  ("\<real>")
   19.15 @@ -786,7 +785,7 @@
   19.16  definition dist_real_def:
   19.17    "dist x y = \<bar>x - y\<bar>"
   19.18  
   19.19 -definition open_real_def [code del]:
   19.20 +definition open_real_def:
   19.21    "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   19.22  
   19.23  instance
    20.1 --- a/src/HOL/Recdef.thy	Mon Jul 12 08:58:27 2010 +0200
    20.2 +++ b/src/HOL/Recdef.thy	Mon Jul 12 10:48:37 2010 +0200
    20.3 @@ -38,7 +38,7 @@
    20.4  
    20.5  definition
    20.6    wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
    20.7 -  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    20.8 +  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    20.9  
   20.10  subsection{*Well-Founded Recursion*}
   20.11  
    21.1 --- a/src/HOL/Rings.thy	Mon Jul 12 08:58:27 2010 +0200
    21.2 +++ b/src/HOL/Rings.thy	Mon Jul 12 10:48:37 2010 +0200
    21.3 @@ -96,7 +96,7 @@
    21.4  begin
    21.5  
    21.6  definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
    21.7 -  [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
    21.8 +  "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
    21.9  
   21.10  lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   21.11    unfolding dvd_def ..
    22.1 --- a/src/HOL/SEQ.thy	Mon Jul 12 08:58:27 2010 +0200
    22.2 +++ b/src/HOL/SEQ.thy	Mon Jul 12 10:48:37 2010 +0200
    22.3 @@ -31,7 +31,7 @@
    22.4  definition
    22.5    Bseq :: "(nat => 'a::real_normed_vector) => bool" where
    22.6      --{*Standard definition for bounded sequence*}
    22.7 -  [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
    22.8 +  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
    22.9  
   22.10  definition
   22.11    monoseq :: "(nat=>real)=>bool" where
   22.12 @@ -39,27 +39,27 @@
   22.13          The use of disjunction here complicates proofs considerably. 
   22.14          One alternative is to add a Boolean argument to indicate the direction. 
   22.15          Another is to develop the notions of increasing and decreasing first.*}
   22.16 -  [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))"
   22.17 +  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
   22.18  
   22.19  definition
   22.20    incseq :: "(nat=>real)=>bool" where
   22.21      --{*Increasing sequence*}
   22.22 -  [code del]: "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
   22.23 +  "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
   22.24  
   22.25  definition
   22.26    decseq :: "(nat=>real)=>bool" where
   22.27      --{*Increasing sequence*}
   22.28 -  [code del]: "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
   22.29 +  "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
   22.30  
   22.31  definition
   22.32    subseq :: "(nat => nat) => bool" where
   22.33      --{*Definition of subsequence*}
   22.34 -  [code del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
   22.35 +  "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
   22.36  
   22.37  definition
   22.38    Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
   22.39      --{*Standard definition of the Cauchy condition*}
   22.40 -  [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
   22.41 +  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
   22.42  
   22.43  
   22.44  subsection {* Bounded Sequences *}
    23.1 --- a/src/HOL/Set.thy	Mon Jul 12 08:58:27 2010 +0200
    23.2 +++ b/src/HOL/Set.thy	Mon Jul 12 10:48:37 2010 +0200
    23.3 @@ -1574,7 +1574,7 @@
    23.4  subsubsection {* Inverse image of a function *}
    23.5  
    23.6  definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where
    23.7 -  [code del]: "f -` B == {x. f x : B}"
    23.8 +  "f -` B == {x. f x : B}"
    23.9  
   23.10  lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
   23.11    by (unfold vimage_def) blast
   23.12 @@ -1657,7 +1657,7 @@
   23.13  subsubsection {* Getting the Contents of a Singleton Set *}
   23.14  
   23.15  definition contents :: "'a set \<Rightarrow> 'a" where
   23.16 -  [code del]: "contents X = (THE x. X = {x})"
   23.17 +  "contents X = (THE x. X = {x})"
   23.18  
   23.19  lemma contents_eq [simp]: "contents {x} = x"
   23.20    by (simp add: contents_def)
    24.1 --- a/src/HOL/Wellfounded.thy	Mon Jul 12 08:58:27 2010 +0200
    24.2 +++ b/src/HOL/Wellfounded.thy	Mon Jul 12 10:48:37 2010 +0200
    24.3 @@ -682,9 +682,8 @@
    24.4  
    24.5  text{* Lexicographic combinations *}
    24.6  
    24.7 -definition
    24.8 -  lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
    24.9 -  [code del]: "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
   24.10 +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
   24.11 +  "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
   24.12  
   24.13  lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
   24.14  apply (unfold wf_def lex_prod_def) 
   24.15 @@ -819,10 +818,8 @@
   24.16  by (force elim!: max_ext.cases)
   24.17  
   24.18  
   24.19 -definition
   24.20 -  min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
   24.21 -where
   24.22 -  [code del]: "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
   24.23 +definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"  where
   24.24 +  "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
   24.25  
   24.26  lemma min_ext_wf:
   24.27    assumes "wf r"