src/HOL/Library/Fraction_Field.thy
changeset 37765 26bdfb7b680b
parent 36414 a19ba9bbc8dc
child 39910 10097e0a9dbd
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  definition
     1.6    Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
     1.7 -  [code del]: "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
     1.8 +  "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
     1.9  
    1.10  code_datatype Fract
    1.11  
    1.12 @@ -93,13 +93,13 @@
    1.13  begin
    1.14  
    1.15  definition
    1.16 -  Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
    1.17 +  Zero_fract_def [code_unfold]: "0 = Fract 0 1"
    1.18  
    1.19  definition
    1.20 -  One_fract_def [code, code_unfold]: "1 = Fract 1 1"
    1.21 +  One_fract_def [code_unfold]: "1 = Fract 1 1"
    1.22  
    1.23  definition
    1.24 -  add_fract_def [code del]:
    1.25 +  add_fract_def:
    1.26    "q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
    1.27      fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
    1.28  
    1.29 @@ -115,7 +115,7 @@
    1.30  qed
    1.31  
    1.32  definition
    1.33 -  minus_fract_def [code del]:
    1.34 +  minus_fract_def:
    1.35    "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})"
    1.36  
    1.37  lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
    1.38 @@ -129,7 +129,7 @@
    1.39    by (cases "b = 0") (simp_all add: eq_fract)
    1.40  
    1.41  definition
    1.42 -  diff_fract_def [code del]: "q - r = q + - (r::'a fract)"
    1.43 +  diff_fract_def: "q - r = q + - (r::'a fract)"
    1.44  
    1.45  lemma diff_fract [simp]:
    1.46    assumes "b \<noteq> 0" and "d \<noteq> 0"
    1.47 @@ -137,7 +137,7 @@
    1.48    using assms by (simp add: diff_fract_def diff_minus)
    1.49  
    1.50  definition
    1.51 -  mult_fract_def [code del]:
    1.52 +  mult_fract_def:
    1.53    "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
    1.54      fractrel``{(fst x * fst y, snd x * snd y)})"
    1.55  
    1.56 @@ -236,7 +236,7 @@
    1.57  begin
    1.58  
    1.59  definition
    1.60 -  inverse_fract_def [code del]:
    1.61 +  inverse_fract_def:
    1.62    "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.
    1.63       fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
    1.64  
    1.65 @@ -250,7 +250,7 @@
    1.66  qed
    1.67  
    1.68  definition
    1.69 -  divide_fract_def [code del]: "q / r = q * inverse (r:: 'a fract)"
    1.70 +  divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
    1.71  
    1.72  lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
    1.73    by (simp add: divide_fract_def)
    1.74 @@ -318,12 +318,12 @@
    1.75  begin
    1.76  
    1.77  definition
    1.78 -  le_fract_def [code del]:
    1.79 +  le_fract_def:
    1.80     "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
    1.81        {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
    1.82  
    1.83  definition
    1.84 -  less_fract_def [code del]: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
    1.85 +  less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
    1.86  
    1.87  lemma le_fract [simp]:
    1.88    assumes "b \<noteq> 0" and "d \<noteq> 0"