Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Rat.thy
changeset 53374 a14d2a854c02
parent 53017 0f376701e83b
child 53652 18fbca265e2e 
--- a/src/HOL/Rat.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Rat.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -237,7 +237,7 @@
 next
   case False
   then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
-  moreover with False have "0 \<noteq> Fract a b" by simp
+  with False have "0 \<noteq> Fract a b" by simp
   with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
   with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
 qed
isabelle