simplified the special-case simprules
authorpaulson
Mon Jan 09 13:28:06 2006 +0100 (2006-01-09)
changeset 186239a5419d5ca01
parent 18622 4524643feecc
child 18624 2e7afae14fa5
simplified the special-case simprules
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Mon Jan 09 13:27:44 2006 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Jan 09 13:28:06 2006 +0100
     1.3 @@ -1556,10 +1556,10 @@
     1.4  done
     1.5  
     1.6  text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
     1.7 -lemmas zero_less_divide_1_iff = zero_less_divide_iff [of "1"]
     1.8 -lemmas divide_less_0_1_iff = divide_less_0_iff [of "1"]
     1.9 -lemmas zero_le_divide_1_iff = zero_le_divide_iff [of "1"]
    1.10 -lemmas divide_le_0_1_iff = divide_le_0_iff [of "1"]
    1.11 +lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]
    1.12 +lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]
    1.13 +lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
    1.14 +lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
    1.15  
    1.16  declare zero_less_divide_1_iff [simp]
    1.17  declare divide_less_0_1_iff [simp]