Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more computation with rationals
authorhaftmann
Thu, 25 Oct 2007 13:52:01 +0200
changeset 25187 2d225c1c4b78
parent 25186 f4d1ebffd025
child 25188 a342dec991aa
more computation with rationals
src/HOL/ex/NormalForm.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/NormalForm.thy	Thu Oct 25 13:52:00 2007 +0200
+++ b/src/HOL/ex/NormalForm.thy	Thu Oct 25 13:52:01 2007 +0200
@@ -110,8 +110,7 @@
 lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
 lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
 lemma "max (Suc 0) 0 = Suc 0" by normalization
-lemma "(42::rat) / 1704 = 7 / 284" by normalization
-
+lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
 normal_form "Suc 0 \<in> set ms"
 
 normal_form "f"
isabelle