doc-src/isar.sty
changeset 10238 9dc33c6c5df9
parent 10221 7171f8ace3c1
child 10335 ccdbf0657982
equal deleted inserted replaced
10237:875bf54b5d74 10238:9dc33c6c5df9
    25 \newcommand{\isaratt}{attribute}
    25 \newcommand{\isaratt}{attribute}
    26 
    26 
    27 \newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}}
    27 \newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}}
    28 \newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}}
    28 \newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}}
    29 
    29 
       
    30 \newcommand{\AND}{\isarkeyword{and}}
    30 \newcommand{\LEMMANAME}{\isarkeyword{lemma}}
    31 \newcommand{\LEMMANAME}{\isarkeyword{lemma}}
    31 \newcommand{\THEOREMNAME}{\isarkeyword{theorem}}
    32 \newcommand{\THEOREMNAME}{\isarkeyword{theorem}}
    32 \newcommand{\NOTENAME}{\isarkeyword{note}}
    33 \newcommand{\NOTENAME}{\isarkeyword{note}}
    33 \newcommand{\FROMNAME}{\isarkeyword{from}}
    34 \newcommand{\FROMNAME}{\isarkeyword{from}}
    34 \newcommand{\WITHNAME}{\isarkeyword{with}}
    35 \newcommand{\WITHNAME}{\isarkeyword{with}}
    47 \newcommand{\ISNAME}{\isarkeyword{is}}
    48 \newcommand{\ISNAME}{\isarkeyword{is}}
    48 \newcommand{\CONCLNAME}{\isarkeyword{concl}}
    49 \newcommand{\CONCLNAME}{\isarkeyword{concl}}
    49 \newcommand{\LETNAME}{\isarkeyword{let}}
    50 \newcommand{\LETNAME}{\isarkeyword{let}}
    50 \newcommand{\DEFNAME}{\isarkeyword{def}}
    51 \newcommand{\DEFNAME}{\isarkeyword{def}}
    51 \newcommand{\OBTAINNAME}{\isarkeyword{obtain}}
    52 \newcommand{\OBTAINNAME}{\isarkeyword{obtain}}
    52 \newcommand{\CMTNAME}{\isarkeyword{-{}-}}
    53 \newcommand{\CMTNAME}{\textbf{---}}
    53 
    54 
    54 \newcommand{\THEORY}{\isarkeyword{theory}}
    55 \newcommand{\THEORY}{\isarkeyword{theory}}
    55 \newcommand{\CONTEXT}{\isarkeyword{context}}
    56 \newcommand{\CONTEXT}{\isarkeyword{context}}
    56 \newcommand{\END}{\isarkeyword{end}}
    57 \newcommand{\END}{\isarkeyword{end}}
    57 
    58 
    89 \newcommand{\IS}[1]{(\ISNAME~#1)}
    90 \newcommand{\IS}[1]{(\ISNAME~#1)}
    90 \newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}
    91 \newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}
    91 \newcommand{\LET}[1]{\LETNAME~#1}
    92 \newcommand{\LET}[1]{\LETNAME~#1}
    92 \newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
    93 \newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
    93 \newcommand{\ATT}[1]{\ap [#1]}
    94 \newcommand{\ATT}[1]{\ap [#1]}
    94 \newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
    95 \newcommand{\CMT}[1]{\CMTNAME~\Text{#1}}
    95 \newcommand{\ALSO}{\isarkeyword{also}}
    96 \newcommand{\ALSO}{\isarkeyword{also}}
    96 \newcommand{\FINALLY}{\isarkeyword{finally}}
    97 \newcommand{\FINALLY}{\isarkeyword{finally}}
    97 \newcommand{\MOREOVER}{\isarkeyword{moreover}}
    98 \newcommand{\MOREOVER}{\isarkeyword{moreover}}
    98 \newcommand{\ULTIMATELY}{\isarkeyword{ultimately}}
    99 \newcommand{\ULTIMATELY}{\isarkeyword{ultimately}}
    99 \newcommand{\OBTAIN}[3]{\OBTAINNAME~#1~\isarkeyword{where}\I@optname{#2}~#3}
   100 \newcommand{\OBTAIN}[3]{\OBTAINNAME~#1~\isarkeyword{where}\I@optname{#2}~#3}