lib/texinputs/isabelle.sty
changeset 14345 3023d90dc59e
parent 14332 fd3535af90ab
child 14347 1fff56703e29
equal deleted inserted replaced
14344:0f0a2148a099 14345:3023d90dc59e
    50 
    50 
    51 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
    51 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
    52 
    52 
    53 \newcommand{\isaindent}[1]{\hphantom{#1}}
    53 \newcommand{\isaindent}[1]{\hphantom{#1}}
    54 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
    54 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
       
    55 \newcommand{\isasep}{\vspace*{2cm}}
    55 \newcommand{\isadigit}[1]{#1}
    56 \newcommand{\isadigit}[1]{#1}
    56 
    57 
    57 \chardef\isacharbang=`\!
    58 \chardef\isacharbang=`\!
    58 \chardef\isachardoublequote=`\"
    59 \chardef\isachardoublequote=`\"
    59 \chardef\isacharhash=`\#
    60 \chardef\isacharhash=`\#