document/isabelle.sty
changeset 10 569222a42cf5
parent 2 301f567e2a8e
child 13 dd1499f296ea
equal deleted inserted replaced
9:91fb17bb6229 10:569222a42cf5
   101 \chardef\isachartilde=`\~%
   101 \chardef\isachartilde=`\~%
   102 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
   102 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
   103 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
   103 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
   104 }
   104 }
   105 
   105 
   106 \newcommand{\isaliteral}[2]{#2}
       
   107 \newcommand{\isanil}{}
       
   108 
       
   109 
   106 
   110 % keyword and section markup
   107 % keyword and section markup
   111 
   108 
   112 \newcommand{\isakeyword}[1]
   109 \newcommand{\isakeyword}[1]
   113 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
   110 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
   156 \def\isastyleminor{\it}%
   153 \def\isastyleminor{\it}%
   157 \def\isastylescript{\footnotesize\it}%
   154 \def\isastylescript{\footnotesize\it}%
   158 \isachardefaults%
   155 \isachardefaults%
   159 \def\isacharunderscorekeyword{\mbox{-}}%
   156 \def\isacharunderscorekeyword{\mbox{-}}%
   160 \def\isacharbang{\isamath{!}}%
   157 \def\isacharbang{\isamath{!}}%
   161 \def\isachardoublequote{\isanil}%
   158 \def\isachardoublequote{}%
   162 \def\isachardoublequoteopen{\isanil}%
   159 \def\isachardoublequoteopen{}%
   163 \def\isachardoublequoteclose{\isanil}%
   160 \def\isachardoublequoteclose{}%
   164 \def\isacharhash{\isamath{\#}}%
   161 \def\isacharhash{\isamath{\#}}%
   165 \def\isachardollar{\isamath{\$}}%
   162 \def\isachardollar{\isamath{\$}}%
   166 \def\isacharpercent{\isamath{\%}}%
   163 \def\isacharpercent{\isamath{\%}}%
   167 \def\isacharampersand{\isamath{\&}}%
   164 \def\isacharampersand{\isamath{\&}}%
   168 \def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
   165 \def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%