tuned doc isar-ref;
authorwenzelm
Wed, 17 Jul 2019 11:18:39 +0200
changeset 70370 ab40ff2fdc67
parent 70369 6c65447b8a64
child 70371 3f9d03571eaa
tuned doc isar-ref;
lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Wed Jul 17 11:09:43 2019 +0200
+++ b/lib/texinputs/isabellesym.sty	Wed Jul 17 11:18:39 2019 +0200
@@ -286,6 +286,7 @@
 \newcommand{\isasymtimes}{\isamath{\times}}
 \newcommand{\isasymdiv}{\isamath{\div}}
 \newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}}  %requires amssymb
 \newcommand{\isasymstar}{\isamath{\star}}
 \newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
 \newcommand{\isasymcirc}{\isamath{\circ}}
@@ -364,7 +365,6 @@
 \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
 \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
 \newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
-\newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}}  %requires amssymb
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
 \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}