src/HOL/Library/Fraction_Field.thy
changeset 40822 98a5faa5aec0
parent 40815 6e2d17cc0d1d
child 45694 4a8743618257
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Nov 30 15:58:21 2010 +0100
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Nov 30 17:19:11 2010 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4  lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
     1.5  proof -
     1.6    have "(\<lambda>x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel"
     1.7 -    by (simp add: congruent_def)
     1.8 +    by (simp add: congruent_def split_paired_all)
     1.9    then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel)
    1.10  qed
    1.11