equal
deleted
inserted
replaced
2 |
2 |
3 \newcommand{\indexdef}[3]% |
3 \newcommand{\indexdef}[3]% |
4 {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}} |
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)}}} |
5 \newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}} |
6 |
6 |
7 \newcommand{\isatt}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}} |
7 \newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}} |
8 \newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt isabelle #1}} |
8 \newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt isabelle #1}} |
9 |
9 |
10 \newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}} |
10 \newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}} |
11 \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}} |
11 \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}} |
12 \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}} |
12 \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}} |