# HG changeset patch
# User wenzelm
# Date 1470167715 -7200
# Node ID 4854f7ee0987438a0887913441e903977e73a507
# Parent  58aab4745e85d9e1105bf3424ef8853bef43c8fe
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);

diff -r 58aab4745e85 -r 4854f7ee0987 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Tue Aug 02 21:30:30 2016 +0200
+++ b/lib/texinputs/isabelle.sty	Tue Aug 02 21:55:15 2016 +0200
@@ -73,6 +73,7 @@
 \newcommand{\isadigit}[1]{#1}
 
 \newcommand{\isachardefaults}{%
+\def\isacharbell{\isamath{\bigbox}}  %requires stmaryrd
 \chardef\isacharbang=`\!%
 \chardef\isachardoublequote=`\"%
 \chardef\isachardoublequoteopen=`\"%
diff -r 58aab4745e85 -r 4854f7ee0987 src/HOL/Nonstandard_Analysis/document/root.tex
--- a/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Aug 02 21:30:30 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Aug 02 21:55:15 2016 +0200
@@ -1,6 +1,7 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage{amsmath}
+\usepackage{stmaryrd}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
diff -r 58aab4745e85 -r 4854f7ee0987 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Aug 02 21:30:30 2016 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Aug 02 21:55:15 2016 +0200
@@ -45,7 +45,8 @@
 
 val char_table =
   Symtab.make
-   [("!", "{\\isacharbang}"),
+   [("\007", "{\\isacharbell}"),
+    ("!", "{\\isacharbang}"),
     ("\"", "{\\isachardoublequote}"),
     ("#", "{\\isacharhash}"),
     ("$", "{\\isachardollar}"),