# 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 \ set ms" normal_form "f"