# HG changeset patch
# User haftmann
# Date 1405787442 -7200
# Node ID 083dfad2727ce1e655846dd614aa42a3efde372b
# Parent  b0d31645f47a50dc8694896076218f6d7afb9d9f
more appropriate postprocessing of rational numbers: extract sign to front of fraction

diff -r b0d31645f47a -r 083dfad2727c src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat Jul 19 11:20:09 2014 +0200
+++ b/src/HOL/Rat.thy	Sat Jul 19 18:30:42 2014 +0200
@@ -957,13 +957,11 @@
   "Frct (a, 0) = 0"
   "Frct (1, 1) = 1"
   "Frct (numeral k, 1) = numeral k"
-  "Frct (- numeral k, 1) = - numeral k"
   "Frct (1, numeral k) = 1 / numeral k"
-  "Frct (1, - numeral k) = 1 / - numeral k"
   "Frct (numeral k, numeral l) = numeral k / numeral l"
-  "Frct (numeral k, - numeral l) = numeral k / - numeral l"
-  "Frct (- numeral k, numeral l) = - numeral k / numeral l"
-  "Frct (- numeral k, - numeral l) = - numeral k / - numeral l"
+  "Frct (- a, b) = - Frct (a, b)"
+  "Frct (a, - b) = - Frct (a, b)"
+  "- (- Frct q) = Frct q"
   by (simp_all add: Fract_of_int_quotient)