# HG changeset patch
# User haftmann
# Date 1409639082 -7200
# Node ID b563ec62d04e18ae5d1d2959ddb86bfd6de711eb
# Parent  c7cc358a6972fea0ef62f67297f0337fd4b8cdcb
more convenient printing of real numbers after evaluation

diff -r c7cc358a6972 -r b563ec62d04e src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Sep 01 19:58:25 2014 +0200
+++ b/src/HOL/Real.thy	Tue Sep 02 08:24:42 2014 +0200
@@ -2035,6 +2035,10 @@
   by simp
 
 lemma [code_abbrev]:
+  "(of_rat (- 1) :: real) = - 1"
+  by simp
+
+lemma [code_abbrev]:
   "(of_rat (numeral k) :: real) = numeral k"
   by simp
 
@@ -2043,17 +2047,10 @@
   by simp
 
 lemma [code_post]:
-  "(of_rat (0 / r)  :: real) = 0"
-  "(of_rat (r / 0)  :: real) = 0"
-  "(of_rat (1 / 1)  :: real) = 1"
-  "(of_rat (numeral k / 1) :: real) = numeral k"
-  "(of_rat (- numeral k / 1) :: real) = - numeral k"
   "(of_rat (1 / numeral k) :: real) = 1 / numeral k"
-  "(of_rat (1 / - numeral k) :: real) = 1 / - numeral k"
-  "(of_rat (numeral k / numeral l)  :: real) = numeral k / numeral l"
-  "(of_rat (numeral k / - numeral l)  :: real) = numeral k / - numeral l"
-  "(of_rat (- numeral k / numeral l)  :: real) = - numeral k / numeral l"
-  "(of_rat (- numeral k / - numeral l)  :: real) = - numeral k / - numeral l"
+  "(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l"
+  "(of_rat (- (1 / numeral k)) :: real) = - (1 / numeral k)"
+  "(of_rat (- (numeral k / numeral l)) :: real) = - (numeral k / numeral l)"
   by (simp_all add: of_rat_divide of_rat_minus)