| changeset 23504 | 2b2323124e8e |
| parent 23501 | e5874335a655 |
| child 27376 | ffe9b958bada |
--- a/doc-src/TutorialI/Types/Numbers.thy Tue Jun 26 13:02:28 2007 +0200 +++ b/doc-src/TutorialI/Types/Numbers.thy Tue Jun 26 15:48:09 2007 +0200 @@ -246,12 +246,18 @@ @{thm[display] mult_cancel_right[no_vars]} \rulename{mult_cancel_right} + +@{thm[display] mult_cancel_left[no_vars]} +\rulename{mult_cancel_left} *} ML{*set show_sorts*} text{* effect of show sorts on the above + +@{thm[display] mult_cancel_left[no_vars]} +\rulename{mult_cancel_left} *} ML{*reset show_sorts*}