doc-src/TutorialI/appendix.tex
changeset 10328 bf33cbd76c05
parent 10242 028f54cd2cc9
child 10538 d1bf9ca9008d
--- a/doc-src/TutorialI/appendix.tex	Wed Oct 25 17:44:59 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex	Wed Oct 25 18:24:33 2000 +0200
@@ -16,7 +16,7 @@
 \indexboldpos{\isasymImp}{$IsaImp} &
 \ttindexboldpos{==>}{$IsaImp} &
 \verb$\<Longrightarrow>$ \\
-\indexboldpos{\isasymAnd}{$IsaAnd} &
+\isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
 \verb$\<And>$ \\
 \indexboldpos{\isasymequiv}{$IsaEq} &
@@ -80,10 +80,10 @@
 \indexboldpos{\isasyminter}{$HOL3Set1}&
 \ttindexbold{Int} &
 \verb$\<inter>$\\
-\indexboldpos{\isasymUnion}{$HOL3Set2}&
+\isasymUnion\index{$HOL3Set2@\isasymUnion|bold}&
 \ttindexbold{UN}, \ttindexbold{Union} &
 \verb$\<Union>$\\
-\indexboldpos{\isasymInter}{$HOL3Set2}&
+\isasymInter\index{$HOL3Set2@\isasymInter|bold}&
 \ttindexbold{INT}, \ttindexbold{Inter} &
 \verb$\<Inter>$\\
 \hline