Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Rat.thy
changeset 57576 083dfad2727c
parent 57514 bdc2c6b40bf2
child 58410 6d46ad54a2ab 
--- 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