| changeset 11428 | 332347b9b942 |
| parent 11310 | 51e70b7bc315 |
| child 15905 | 0a4cc9b113c7 |
--- a/doc-src/TutorialI/Misc/Option2.thy Mon Jul 16 13:14:19 2001 +0200 +++ b/doc-src/TutorialI/Misc/Option2.thy Tue Jul 17 13:46:21 2001 +0200 @@ -4,7 +4,8 @@ hide type option (*>*) -text{*\indexbold{*option}\indexbold{*None}\indexbold{*Some} +text{*\indexbold{*option (type)}\indexbold{*None (constant)}% +\indexbold{*Some (constant)} Our final datatype is very simple but still eminently useful: *}