src/HOL/Rat.thy
changeset 67051 e7e54a0b9197
parent 66806 a4e82b58d833
child 68441 3b11d48a711a
     1.1 --- a/src/HOL/Rat.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Rat.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -999,7 +999,7 @@
     1.4  proof (cases p)
     1.5    case (Fract a b)
     1.6    then show ?thesis
     1.7 -    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd.commute)
     1.8 +    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract ac_simps)
     1.9  qed
    1.10  
    1.11  lemma rat_divide_code [code abstract]:
    1.12 @@ -1008,9 +1008,10 @@
    1.13       in normalize (a * d, c * b))"
    1.14    by (cases p, cases q) (simp add: quotient_of_Fract)
    1.15  
    1.16 -lemma rat_abs_code [code abstract]: "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
    1.17 +lemma rat_abs_code [code abstract]:
    1.18 +  "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
    1.19    by (cases p) (simp add: quotient_of_Fract)
    1.20 -
    1.21 +  
    1.22  lemma rat_sgn_code [code abstract]: "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)"
    1.23  proof (cases p)
    1.24    case (Fract a b)