proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
authorwenzelm
Tue Aug 02 21:55:15 2016 +0200 (2016-08-02)
changeset 635904854f7ee0987
parent 63589 58aab4745e85
child 63591 8d20875f1290
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
lib/texinputs/isabelle.sty
src/HOL/Nonstandard_Analysis/document/root.tex
src/Pure/Thy/latex.ML
     1.1 --- a/lib/texinputs/isabelle.sty	Tue Aug 02 21:30:30 2016 +0200
     1.2 +++ b/lib/texinputs/isabelle.sty	Tue Aug 02 21:55:15 2016 +0200
     1.3 @@ -73,6 +73,7 @@
     1.4  \newcommand{\isadigit}[1]{#1}
     1.5  
     1.6  \newcommand{\isachardefaults}{%
     1.7 +\def\isacharbell{\isamath{\bigbox}}  %requires stmaryrd
     1.8  \chardef\isacharbang=`\!%
     1.9  \chardef\isachardoublequote=`\"%
    1.10  \chardef\isachardoublequoteopen=`\"%
     2.1 --- a/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Aug 02 21:30:30 2016 +0200
     2.2 +++ b/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Aug 02 21:55:15 2016 +0200
     2.3 @@ -1,6 +1,7 @@
     2.4  \documentclass[11pt,a4paper]{article}
     2.5  \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
     2.6  \usepackage{amsmath}
     2.7 +\usepackage{stmaryrd}
     2.8  \usepackage{pdfsetup}
     2.9  
    2.10  \urlstyle{rm}
     3.1 --- a/src/Pure/Thy/latex.ML	Tue Aug 02 21:30:30 2016 +0200
     3.2 +++ b/src/Pure/Thy/latex.ML	Tue Aug 02 21:55:15 2016 +0200
     3.3 @@ -45,7 +45,8 @@
     3.4  
     3.5  val char_table =
     3.6    Symtab.make
     3.7 -   [("!", "{\\isacharbang}"),
     3.8 +   [("\007", "{\\isacharbell}"),
     3.9 +    ("!", "{\\isacharbang}"),
    3.10      ("\"", "{\\isachardoublequote}"),
    3.11      ("#", "{\\isacharhash}"),
    3.12      ("$", "{\\isachardollar}"),