doc-src/isar.sty
changeset 10860 12f45010ecb5
parent 10335 ccdbf0657982
child 12615 3ef6235a4a75
equal deleted inserted replaced
10859:b88ce3ed3b1d 10860:12f45010ecb5
    83 \newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
    83 \newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
    84 \newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
    84 \newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
    85 \newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}}
    85 \newcommand{\BYY}[2]{\BYNAME\I@optmeth{#1}\I@optmeth{#2}}
    86 \newcommand{\APPLY}[1]{\APPLYNAME\I@optmeth{#1}}
    86 \newcommand{\APPLY}[1]{\APPLYNAME\I@optmeth{#1}}
    87 \newcommand{\DONE}{\isarkeyword{done}}
    87 \newcommand{\DONE}{\isarkeyword{done}}
    88 \newcommand{\DOT}{\isarkeyword{.}}
    88 \newcommand{\DOT}{\textbf{.}}
    89 \newcommand{\DDOT}{\isarkeyword{.\,.}}
    89 \newcommand{\DDOT}{\textbf{.\,.}}
    90 \newcommand{\DDDOT}{\dots}
    90 \newcommand{\DDDOT}{\dots}
    91 \newcommand{\IS}[1]{(\ISNAME~#1)}
    91 \newcommand{\IS}[1]{(\ISNAME~#1)}
    92 \newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}
    92 \newcommand{\ISS}[2]{(\ISNAME~#1~\ISNAME~#2)}
    93 \newcommand{\LET}[1]{\LETNAME~#1}
    93 \newcommand{\LET}[1]{\LETNAME~#1}
    94 \newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
    94 \newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}