1.1 --- a/doc-src/TutorialI/tutorial.sty	Fri Jul 13 18:19:29 2001 +0200
     1.2 +++ b/doc-src/TutorialI/tutorial.sty	Fri Jul 13 18:20:26 2001 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  \newcommand\sdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (symbol)}}
     1.5  
     1.6  \newcommand\tdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)}}
     1.7 -\newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem|bold)}}
     1.8 +\newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}}
     1.9  
    1.10  \newcommand\cldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (class)}}
    1.11  \newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} (type)}}
    1.12 @@ -50,8 +50,8 @@
    1.13  \newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@}
    1.14  \newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@}
    1.15  
    1.16 -\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}\@}
    1.17 -\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}\@}
    1.18 +\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
    1.19 +\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
    1.20  \newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}\@}
    1.21  \newcommand{\isaindex}[1]{\isa{#1}\index{*#1}\@}
    1.22  
    1.23 @@ -76,8 +76,10 @@
    1.24  
    1.25  \newif\ifremarks
    1.26  \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
    1.27 -\newcommand{\rulename}[1]{\hfill(#1\index{#1@\protect\isa{#1} (theorem)|bold})}
    1.28 +
    1.29  %names of Isabelle rules
    1.30 +\newcommand{\rulename}[1]{\hfill(#1)}
    1.31 +\newcommand{\rulenamedx}[1]{\hfill(#1\index{#1@\protect\isa{#1} (theorem)|bold})}
    1.32  
    1.33  %%%% meta-logical connectives
    1.34  
    1.35 @@ -143,7 +145,6 @@
    1.36  \let\union=\bigcup
    1.37  
    1.38  \def\ML{{\sc ml}}
    1.39 -\def\OBJ{{\sc obj}}
    1.40  \def\AST{{\sc ast}}
    1.41  
    1.42  %macros to change the treatment of symbols