1.1 --- a/src/HOL/Rat.thy	Sat Jul 19 11:20:09 2014 +0200
     1.2 +++ b/src/HOL/Rat.thy	Sat Jul 19 18:30:42 2014 +0200
     1.3 @@ -957,13 +957,11 @@
     1.4    "Frct (a, 0) = 0"
     1.5    "Frct (1, 1) = 1"
     1.6    "Frct (numeral k, 1) = numeral k"
     1.7 -  "Frct (- numeral k, 1) = - numeral k"
     1.8    "Frct (1, numeral k) = 1 / numeral k"
     1.9 -  "Frct (1, - numeral k) = 1 / - numeral k"
    1.10    "Frct (numeral k, numeral l) = numeral k / numeral l"
    1.11 -  "Frct (numeral k, - numeral l) = numeral k / - numeral l"
    1.12 -  "Frct (- numeral k, numeral l) = - numeral k / numeral l"
    1.13 -  "Frct (- numeral k, - numeral l) = - numeral k / - numeral l"
    1.14 +  "Frct (- a, b) = - Frct (a, b)"
    1.15 +  "Frct (a, - b) = - Frct (a, b)"
    1.16 +  "- (- Frct q) = Frct q"
    1.17    by (simp_all add: Fract_of_int_quotient)
    1.18  
    1.19