# HG changeset patch
# User haftmann
# Date 1193203194 -7200
# Node ID f3739a8da38fcbb2df8c6f881aefcad306fb18ee
# Parent  0fcb4775cbfbd69ab180dace61aa1f5917610400
example with rational numbers

diff -r 0fcb4775cbfb -r f3739a8da38f src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Wed Oct 24 07:19:53 2007 +0200
+++ b/src/HOL/ex/NormalForm.thy	Wed Oct 24 07:19:54 2007 +0200
@@ -5,7 +5,7 @@
 header {* Test of normalization function *}
 
 theory NormalForm
-imports Main
+imports Main "~~/src/HOL/Real/Rational"
 begin
 
 lemma "True" by normalization
@@ -110,6 +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
 
 normal_form "Suc 0 \<in> set ms"