# HG changeset patch
# User wenzelm
# Date 1512641672 -3600
# Node ID c7def8f836d09be51fdf5e705f9febaaa8a3abe9
# Parent  39117b6f0b2ea030ec3a527f9be00e669911dd00
tuned output in isar-ref manual;

diff -r 39117b6f0b2e -r c7def8f836d0 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Thu Dec 07 11:12:55 2017 +0100
+++ b/lib/texinputs/isabellesym.sty	Thu Dec 07 11:14:32 2017 +0100
@@ -358,11 +358,11 @@
 \newcommand{\isasymcedilla}{\isatext{\c\relax}}
 \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
-\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
 \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
 \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
 \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
 \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
+\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymcomment}{\isatext{---}}
 \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}