31 |
31 |
32 \newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}} |
32 \newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}} |
33 \newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}} |
33 \newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}} |
34 |
34 |
35 \newcommand{\AND}{\isarkeyword{and}} |
35 \newcommand{\AND}{\isarkeyword{and}} |
|
36 \newcommand{\IN}{\isarkeyword{in}} |
36 \newcommand{\COROLLARYNAME}{\isarkeyword{corollary}} |
37 \newcommand{\COROLLARYNAME}{\isarkeyword{corollary}} |
37 \newcommand{\LEMMANAME}{\isarkeyword{lemma}} |
38 \newcommand{\LEMMANAME}{\isarkeyword{lemma}} |
38 \newcommand{\THEOREMNAME}{\isarkeyword{theorem}} |
39 \newcommand{\THEOREMNAME}{\isarkeyword{theorem}} |
39 \newcommand{\NOTENAME}{\isarkeyword{note}} |
40 \newcommand{\NOTENAME}{\isarkeyword{note}} |
40 \newcommand{\FROMNAME}{\isarkeyword{from}} |
41 \newcommand{\FROMNAME}{\isarkeyword{from}} |
41 \newcommand{\WITHNAME}{\isarkeyword{with}} |
42 \newcommand{\WITHNAME}{\isarkeyword{with}} |
42 \newcommand{\USINGNAME}{\isarkeyword{using}} |
43 \newcommand{\USINGNAME}{\isarkeyword{using}} |
|
44 \newcommand{\FIXESNAME}{\isarkeyword{fixes}} |
|
45 \newcommand{\ASSUMESNAME}{\isarkeyword{assumes}} |
|
46 \newcommand{\DEFINESNAME}{\isarkeyword{defines}} |
|
47 \newcommand{\NOTESNAME}{\isarkeyword{notes}} |
|
48 \newcommand{\INCLUDESNAME}{\isarkeyword{includes}} |
43 \newcommand{\FIXNAME}{\isarkeyword{fix}} |
49 \newcommand{\FIXNAME}{\isarkeyword{fix}} |
44 \newcommand{\ASSUMENAME}{\isarkeyword{assume}} |
50 \newcommand{\ASSUMENAME}{\isarkeyword{assume}} |
45 \newcommand{\PRESUMENAME}{\isarkeyword{presume}} |
51 \newcommand{\PRESUMENAME}{\isarkeyword{presume}} |
46 \newcommand{\CASENAME}{\isarkeyword{case}} |
52 \newcommand{\CASENAME}{\isarkeyword{case}} |
47 \newcommand{\HAVENAME}{\isarkeyword{have}} |
53 \newcommand{\HAVENAME}{\isarkeyword{have}} |
68 \newcommand{\CONSTDEFS}{\isarkeyword{constdefs}} |
74 \newcommand{\CONSTDEFS}{\isarkeyword{constdefs}} |
69 \newcommand{\DEFS}{\isarkeyword{defs}} |
75 \newcommand{\DEFS}{\isarkeyword{defs}} |
70 \newcommand{\AXCLASS}{\isarkeyword{axclass}} |
76 \newcommand{\AXCLASS}{\isarkeyword{axclass}} |
71 \newcommand{\INSTANCE}{\isarkeyword{instance}} |
77 \newcommand{\INSTANCE}{\isarkeyword{instance}} |
72 \newcommand{\DECLARE}{\isarkeyword{declare}} |
78 \newcommand{\DECLARE}{\isarkeyword{declare}} |
|
79 \newcommand{\LEMMAS}{\isarkeyword{lemmas}} |
|
80 \newcommand{\THEOREMS}{\isarkeyword{theorems}} |
|
81 \newcommand{\LOCALE}{\isarkeyword{locale}} |
73 \newcommand{\TEXT}{\isarkeyword{text}} |
82 \newcommand{\TEXT}{\isarkeyword{text}} |
74 \newcommand{\TXT}{\isarkeyword{txt}} |
83 \newcommand{\TXT}{\isarkeyword{txt}} |
75 \newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2} |
84 \newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2} |
76 \newcommand{\FROM}[1]{\FROMNAME~#1} |
85 \newcommand{\FROM}[1]{\FROMNAME~#1} |
77 \newcommand{\WITH}[1]{\WITHNAME~#1} |
86 \newcommand{\WITH}[1]{\WITHNAME~#1} |
78 \newcommand{\USING}[1]{\USINGNAME~#1} |
87 \newcommand{\USING}[1]{\USINGNAME~#1} |
|
88 \newcommand{\FIXES}[1]{\FIXESNAME~#1} |
|
89 \newcommand{\ASSUMES}[2]{\ASSUMESNAME\I@optname{#1}~#2} |
|
90 \newcommand{\DEFINES}[2]{\DEFINESNAME\I@optname{#1}~#2} |
|
91 \newcommand{\NOTES}[2]{\NOTESNAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2} |
|
92 \newcommand{\INCLUDES}[1]{\INCLUDESNAME~#1} |
79 \newcommand{\FIX}[1]{\FIXNAME~#1} |
93 \newcommand{\FIX}[1]{\FIXNAME~#1} |
80 \newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2} |
94 \newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2} |
81 \newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2} |
95 \newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2} |
82 \newcommand{\CASE}[1]{\CASENAME~#1} |
96 \newcommand{\CASE}[1]{\CASENAME~#1} |
83 \newcommand{\THEN}{\isarkeyword{then}} |
97 \newcommand{\THEN}{\isarkeyword{then}} |