1\usepackage{ifthen} 2 3\newcommand{\indexdef}[3]% 4{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}} 5\newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}} 6 7\newcommand{\isadigitreset}{\def\isadigit##1{##1}} 8 9\newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt #1}} 10\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt isabelle #1}} 11 12\newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}} 13\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}} 14\newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}} 15 16\newcommand{\isasymIF}{\isakeyword{if}} 17\newcommand{\isasymFOR}{\isakeyword{for}} 18\newcommand{\isasymAND}{\isakeyword{and}} 19\newcommand{\isasymIS}{\isakeyword{is}} 20\newcommand{\isasymWHERE}{\isakeyword{where}} 21\newcommand{\isasymBEGIN}{\isakeyword{begin}} 22\newcommand{\isasymIMPORTS}{\isakeyword{imports}} 23\newcommand{\isasymIN}{\isakeyword{in}} 24\newcommand{\isasymFIXES}{\isakeyword{fixes}} 25\newcommand{\isasymASSUMES}{\isakeyword{assumes}} 26\newcommand{\isasymSHOWS}{\isakeyword{shows}} 27\newcommand{\isasymOBTAINS}{\isakeyword{obtains}} 28 29\newcommand{\isasymASSM}{\isacommand{assm}} 30