src/HOL/ex/NormalForm.thy
changeset 25187 2d225c1c4b78
parent 25165 f3739a8da38f
child 25866 263aaf988d44
--- 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"