# HG changeset patch
# User haftmann
# Date 1193313121 -7200
# Node ID 2d225c1c4b78f451130c7de4a84cd67b7c0be687
# Parent  f4d1ebffd0258c8f79a0fb50c6d3c29772ecf316
more computation with rationals

diff -r f4d1ebffd025 -r 2d225c1c4b78 src/HOL/ex/NormalForm.thy
--- 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"