summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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