doc-src/isabelle.sty
changeset 40686 2ff10e613689
parent 40681 b646316f8b3c
equal deleted inserted replaced
40685:313a24b66a8d 40686:2ff10e613689
    94 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
    94 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
    95 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
    95 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
    96 }
    96 }
    97 
    97 
    98 \newcommand{\isaliteral}[2]{#2}
    98 \newcommand{\isaliteral}[2]{#2}
       
    99 \newcommand{\isanil}{}
    99 
   100 
   100 
   101 
   101 % keyword and section markup
   102 % keyword and section markup
   102 
   103 
   103 \newcommand{\isakeyword}[1]
   104 \newcommand{\isakeyword}[1]
   146 \renewcommand{\isastyle}{\small\it}%
   147 \renewcommand{\isastyle}{\small\it}%
   147 \renewcommand{\isastyleminor}{\it}%
   148 \renewcommand{\isastyleminor}{\it}%
   148 \renewcommand{\isastylescript}{\footnotesize\it}%
   149 \renewcommand{\isastylescript}{\footnotesize\it}%
   149 \renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
   150 \renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
   150 \renewcommand{\isacharbang}{\isamath{!}}%
   151 \renewcommand{\isacharbang}{\isamath{!}}%
   151 \renewcommand{\isachardoublequote}{}%
   152 \renewcommand{\isachardoublequote}{\isanil}%
   152 \renewcommand{\isachardoublequoteopen}{}%
   153 \renewcommand{\isachardoublequoteopen}{\isanil}%
   153 \renewcommand{\isachardoublequoteclose}{}%
   154 \renewcommand{\isachardoublequoteclose}{\isanil}%
   154 \renewcommand{\isacharhash}{\isamath{\#}}%
   155 \renewcommand{\isacharhash}{\isamath{\#}}%
   155 \renewcommand{\isachardollar}{\isamath{\$}}%
   156 \renewcommand{\isachardollar}{\isamath{\$}}%
   156 \renewcommand{\isacharpercent}{\isamath{\%}}%
   157 \renewcommand{\isacharpercent}{\isamath{\%}}%
   157 \renewcommand{\isacharampersand}{\isamath{\&}}%
   158 \renewcommand{\isacharampersand}{\isamath{\&}}%
   158 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
   159 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%