more convenient printing of real numbers after evaluation
authorhaftmann
Tue Sep 02 08:24:42 2014 +0200 (2014-09-02)
changeset 58134b563ec62d04e
parent 58133 c7cc358a6972
child 58135 0774d32fe74f
child 58136 10f92532f128
more convenient printing of real numbers after evaluation
src/HOL/Real.thy
     1.1 --- a/src/HOL/Real.thy	Mon Sep 01 19:58:25 2014 +0200
     1.2 +++ b/src/HOL/Real.thy	Tue Sep 02 08:24:42 2014 +0200
     1.3 @@ -2035,6 +2035,10 @@
     1.4    by simp
     1.5  
     1.6  lemma [code_abbrev]:
     1.7 +  "(of_rat (- 1) :: real) = - 1"
     1.8 +  by simp
     1.9 +
    1.10 +lemma [code_abbrev]:
    1.11    "(of_rat (numeral k) :: real) = numeral k"
    1.12    by simp
    1.13  
    1.14 @@ -2043,17 +2047,10 @@
    1.15    by simp
    1.16  
    1.17  lemma [code_post]:
    1.18 -  "(of_rat (0 / r)  :: real) = 0"
    1.19 -  "(of_rat (r / 0)  :: real) = 0"
    1.20 -  "(of_rat (1 / 1)  :: real) = 1"
    1.21 -  "(of_rat (numeral k / 1) :: real) = numeral k"
    1.22 -  "(of_rat (- numeral k / 1) :: real) = - numeral k"
    1.23    "(of_rat (1 / numeral k) :: real) = 1 / numeral k"
    1.24 -  "(of_rat (1 / - numeral k) :: real) = 1 / - numeral k"
    1.25 -  "(of_rat (numeral k / numeral l)  :: real) = numeral k / numeral l"
    1.26 -  "(of_rat (numeral k / - numeral l)  :: real) = numeral k / - numeral l"
    1.27 -  "(of_rat (- numeral k / numeral l)  :: real) = - numeral k / numeral l"
    1.28 -  "(of_rat (- numeral k / - numeral l)  :: real) = - numeral k / - numeral l"
    1.29 +  "(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l"
    1.30 +  "(of_rat (- (1 / numeral k)) :: real) = - (1 / numeral k)"
    1.31 +  "(of_rat (- (numeral k / numeral l)) :: real) = - (numeral k / numeral l)"
    1.32    by (simp_all add: of_rat_divide of_rat_minus)
    1.33  
    1.34