src/HOL/Rat.thy
changeset 53374 a14d2a854c02
parent 53017 0f376701e83b
child 53652 18fbca265e2e
     1.1 --- a/src/HOL/Rat.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Rat.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -237,7 +237,7 @@
     1.4  next
     1.5    case False
     1.6    then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
     1.7 -  moreover with False have "0 \<noteq> Fract a b" by simp
     1.8 +  with False have "0 \<noteq> Fract a b" by simp
     1.9    with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
    1.10    with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
    1.11  qed