merged

--- a/src/HOL/Fields.thy	Tue Apr 27 16:09:15 2010 +0200
+++ b/src/HOL/Fields.thy	Tue Apr 27 16:24:57 2010 +0200
@@ -778,15 +778,22 @@
 done
 
 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
-lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
-lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
-lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
-lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
+
+lemma zero_le_divide_1_iff [simp, no_atp]:
+  "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
+  by (simp add: zero_le_divide_iff)
 
-declare zero_less_divide_1_iff [simp,no_atp]
-declare divide_less_0_1_iff [simp,no_atp]
-declare zero_le_divide_1_iff [simp,no_atp]
-declare divide_le_0_1_iff [simp,no_atp]
+lemma zero_less_divide_1_iff [simp, no_atp]:
+  "0 < 1 / a \<longleftrightarrow> 0 < a"
+  by (simp add: zero_less_divide_iff)
+
+lemma divide_le_0_1_iff [simp, no_atp]:
+  "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
+  by (simp add: divide_le_0_iff)
+
+lemma divide_less_0_1_iff [simp, no_atp]:
+  "1 / a < 0 \<longleftrightarrow> a < 0"
+  by (simp add: divide_less_0_iff)
 
 lemma divide_right_mono:
      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
@@ -804,8 +811,6 @@
   apply (auto simp add: mult_commute)
 done
 
-
-
 text{*Simplify quotients that are compared with the value 1.*}
 
 lemma le_divide_eq_1 [no_atp]:

--- a/src/HOL/Int.thy	Tue Apr 27 16:09:15 2010 +0200
+++ b/src/HOL/Int.thy	Tue Apr 27 16:24:57 2010 +0200
@@ -324,27 +324,6 @@
 
 end
 
-context linordered_idom
-begin
-
-lemma of_int_le_iff [simp]:
-  "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
-by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
-
-text{*Special cases where either operand is zero*}
-lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
-lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
-
-lemma of_int_less_iff [simp]:
-  "of_int w < of_int z \<longleftrightarrow> w < z"
-  by (simp add: not_le [symmetric] linorder_not_le [symmetric])
-
-text{*Special cases where either operand is zero*}
-lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
-lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
-
-end
-
 text{*Class for unital rings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}
 class ring_char_0 = ring_1 + semiring_char_0
@@ -358,13 +337,47 @@
 done
 
 text{*Special cases where either operand is zero*}
-lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
-lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified]
+lemma of_int_eq_0_iff [simp]:
+  "of_int z = 0 \<longleftrightarrow> z = 0"
+  using of_int_eq_iff [of z 0] by simp
+
+lemma of_int_0_eq_iff [simp]:
+  "0 = of_int z \<longleftrightarrow> z = 0"
+  using of_int_eq_iff [of 0 z] by simp
 
 end
 
+context linordered_idom
+begin
+
 text{*Every @{text linordered_idom} has characteristic zero.*}
-subclass (in linordered_idom) ring_char_0 by intro_locales
+subclass ring_char_0 ..
+
+lemma of_int_le_iff [simp]:
+  "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
+  by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
+
+lemma of_int_less_iff [simp]:
+  "of_int w < of_int z \<longleftrightarrow> w < z"
+  by (simp add: less_le order_less_le)
+
+lemma of_int_0_le_iff [simp]:
+  "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
+  using of_int_le_iff [of 0 z] by simp
+
+lemma of_int_le_0_iff [simp]:
+  "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
+  using of_int_le_iff [of z 0] by simp
+
+lemma of_int_0_less_iff [simp]:
+  "0 < of_int z \<longleftrightarrow> 0 < z"
+  using of_int_less_iff [of 0 z] by simp
+
+lemma of_int_less_0_iff [simp]:
+  "of_int z < 0 \<longleftrightarrow> z < 0"
+  using of_int_less_iff [of z 0] by simp
+
+end
 
 lemma of_int_eq_id [simp]: "of_int = id"
 proof

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 16:09:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 16:24:57 2010 +0200
@@ -863,7 +863,7 @@
         |> the_default "Warning: The Isar proof construction failed.\n"
   in (one_line_proof ^ isar_proof, lemma_names) end
 
-fun proof_text isar_proof =
-  if isar_proof then isar_proof_text else K metis_proof_text
+fun proof_text isar_proof isar_params =
+  if isar_proof then isar_proof_text isar_params else metis_proof_text
 
 end;