--- 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*}