| author | haftmann |
| Mon, 21 Apr 2014 21:16:05 +0200 | |
| changeset 56626 | 6532efd66a70 |
| parent 55143 | 04448228381d |
| child 58716 | 23a380cc45f4 |
| permissions | -rw-r--r-- |
| 7050 | 1 |
\usepackage{ifthen}
|
2 |
||
| 26745 | 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)}}}
|
|
| 7138 | 6 |
|
| 28214 | 7 |
\newcommand{\isatt}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}}
|
| 48602 | 8 |
\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt isabelle #1}}
|
| 28214 | 9 |
|
| 26745 | 10 |
\newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
|
11 |
\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
|
|
12 |
\newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
|
|
| 7170 | 13 |
|
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51657
diff
changeset
|
14 |
\newcommand{\isasymFOR}{\isakeyword{for}}
|
| 26755 | 15 |
\newcommand{\isasymAND}{\isakeyword{and}}
|
16 |
\newcommand{\isasymIS}{\isakeyword{is}}
|
|
17 |
\newcommand{\isasymWHERE}{\isakeyword{where}}
|
|
| 26769 | 18 |
\newcommand{\isasymBEGIN}{\isakeyword{begin}}
|
19 |
\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
|
|
| 26783 | 20 |
\newcommand{\isasymIN}{\isakeyword{in}}
|
| 29727 | 21 |
\newcommand{\isasymFIXES}{\isakeyword{fixes}}
|
22 |
\newcommand{\isasymASSUMES}{\isakeyword{assumes}}
|
|
23 |
\newcommand{\isasymSHOWS}{\isakeyword{shows}}
|
|
24 |
\newcommand{\isasymOBTAINS}{\isakeyword{obtains}}
|
|
25 |
||
26 |
\newcommand{\isasymASSM}{\isacommand{assm}}
|