# HG changeset patch
# User nipkow
# Date 1182840124 -7200
# Node ID e5874335a655772902c6140fd3ae023be727223c
# Parent  3e3c9d4da4766ef3f26f031ad67f646bacd720aa
removed removed lemmas

diff -r 3e3c9d4da476 -r e5874335a655 doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Tue Jun 26 00:35:14 2007 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Tue Jun 26 08:42:04 2007 +0200
@@ -246,18 +246,12 @@
 
 @{thm[display] mult_cancel_right[no_vars]}
 \rulename{mult_cancel_right}
-
-@{thm[display] field_mult_cancel_right[no_vars]}
-\rulename{field_mult_cancel_right}
 *}
 
 ML{*set show_sorts*}
 
 text{*
 effect of show sorts on the above
-
-@{thm[display] field_mult_cancel_right[no_vars]}
-\rulename{field_mult_cancel_right}
 *}
 
 ML{*reset show_sorts*}