doc-src/isar.sty
changeset 8618 87cddace4432
parent 8504 242527763a16
child 8900 e9f1cd37cba4
equal deleted inserted replaced
8617:33e2bd53aec3 8618:87cddace4432
    84 \newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
    84 \newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
    85 \newcommand{\ATT}[1]{\ap [#1]}
    85 \newcommand{\ATT}[1]{\ap [#1]}
    86 \newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
    86 \newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
    87 \newcommand{\ALSO}{\isarkeyword{also}}
    87 \newcommand{\ALSO}{\isarkeyword{also}}
    88 \newcommand{\FINALLY}{\isarkeyword{finally}}
    88 \newcommand{\FINALLY}{\isarkeyword{finally}}
       
    89 \newcommand{\MOREOVER}{\isarkeyword{moreover}}
       
    90 \newcommand{\ULTIMATELY}{\isarkeyword{ultimately}}
    89 \newcommand{\OBTAIN}[3]{\OBTAINNAME~#1~\isarkeyword{where}\I@optname{#2}~#3}
    91 \newcommand{\OBTAIN}[3]{\OBTAINNAME~#1~\isarkeyword{where}\I@optname{#2}~#3}
    90 \newcommand{\BG}{\isarkeyword{\{\{}}
    92 \newcommand{\BG}{\isarkeyword{\{\{}}
    91 \newcommand{\EN}{\isarkeyword{\}\}}}
    93 \newcommand{\EN}{\isarkeyword{\}\}}}
    92 \newcommand{\NEXT}{\isarkeyword{next}}
    94 \newcommand{\NEXT}{\isarkeyword{next}}
    93 \newcommand{\SORRY}{\isarkeyword{sorry}}
    95 \newcommand{\SORRY}{\isarkeyword{sorry}}