Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more appropriate postprocessing of rational numbers: extract sign to front of fraction
authorhaftmann
Sat, 19 Jul 2014 18:30:42 +0200
changeset 57576 083dfad2727c
parent 57575 b0d31645f47a
child 57577 e848a17d9dee
more appropriate postprocessing of rational numbers: extract sign to front of fraction
src/HOL/Rat.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle