changeset 13439 | 2f98365f57a8 |
parent 12771 | fc3a60549075 |
child 14353 | 79f9fbef9106 |
--- a/doc-src/TutorialI/Documents/Documents.thy Wed Jul 31 16:10:24 2002 +0200 +++ b/doc-src/TutorialI/Documents/Documents.thy Wed Jul 31 17:42:38 2002 +0200 @@ -118,7 +118,7 @@ output as @{text "A\<^sup>\<star>"}. \medskip Replacing our definition of @{text xor} by the following - specifies a Isabelle symbol for the new operator: + specifies an Isabelle symbol for the new operator: *} (*<*)