doc-src/TutorialI/ToyList/ToyList.thy
changeset 15364 0c3891c3528f
parent 15141 a95c2ff210ba
child 16360 6897b5958be7
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Thu Dec 02 14:47:07 2004 +0100
@@ -24,8 +24,8 @@
 @{term"False"}. Because this notation quickly becomes unwieldy, the
 datatype declaration is annotated with an alternative syntax: instead of
 @{term[source]Nil} and \isa{Cons x xs} we can write
-@{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
-@{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+@{term"[]"}\index{$HOL2list@\isa{[]}|bold} and
+@{term"x # xs"}\index{$HOL2list@\isa{\#}|bold}. In fact, this
 alternative syntax is the familiar one.  Thus the list \isa{Cons True
 (Cons False Nil)} becomes @{term"True # False # []"}. The annotation
 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
@@ -56,7 +56,7 @@
 restriction, the order of items in a theory file is unconstrained. Function
 @{text"app"} is annotated with concrete syntax too. Instead of the
 prefix syntax @{text"app xs ys"} the infix
-@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+@{term"xs @ ys"}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
 form. Both functions are defined recursively:
 *}