| author | wenzelm |
| Tue, 16 Nov 2021 21:21:15 +0100 | |
| changeset 74798 | 507f50dbeb79 |
| parent 73757 | cb933ba9ecfe |
| 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 |
|
| 59346 | 7 |
\newcommand{\isadigitreset}{\def\isadigit##1{##1}}
|
8 |
||
| 59343 | 9 |
\newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt #1}}
|
10 |
\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt isabelle #1}}
|
|
| 28214 | 11 |
|
| 60459 | 12 |
\newcommand{\isasymIF}{\isakeyword{if}}
|
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51657
diff
changeset
|
13 |
\newcommand{\isasymFOR}{\isakeyword{for}}
|
| 26755 | 14 |
\newcommand{\isasymAND}{\isakeyword{and}}
|
15 |
\newcommand{\isasymIS}{\isakeyword{is}}
|
|
16 |
\newcommand{\isasymWHERE}{\isakeyword{where}}
|
|
| 26769 | 17 |
\newcommand{\isasymBEGIN}{\isakeyword{begin}}
|
18 |
\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
|
|
| 26783 | 19 |
\newcommand{\isasymIN}{\isakeyword{in}}
|
| 29727 | 20 |
\newcommand{\isasymFIXES}{\isakeyword{fixes}}
|
21 |
\newcommand{\isasymASSUMES}{\isakeyword{assumes}}
|
|
22 |
\newcommand{\isasymSHOWS}{\isakeyword{shows}}
|
|
23 |
\newcommand{\isasymOBTAINS}{\isakeyword{obtains}}
|
|
24 |
||
25 |
\newcommand{\isasymASSM}{\isacommand{assm}}
|