# HG changeset patch
# User paulson
# Date 1136809686 -3600
# Node ID 9a5419d5ca01b74a787e8326921f105c40ba3f4a
# Parent  4524643feecc47cc4024cce53e5523d51cde91ab
simplified the special-case simprules

diff -r 4524643feecc -r 9a5419d5ca01 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Jan 09 13:27:44 2006 +0100
+++ b/src/HOL/Ring_and_Field.thy	Mon Jan 09 13:28:06 2006 +0100
@@ -1556,10 +1556,10 @@
 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"]
-lemmas divide_less_0_1_iff = divide_less_0_iff [of "1"]
-lemmas zero_le_divide_1_iff = zero_le_divide_iff [of "1"]
-lemmas divide_le_0_1_iff = divide_le_0_iff [of "1"]
+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]
 
 declare zero_less_divide_1_iff [simp]
 declare divide_less_0_1_iff [simp]