--- a/lib/texinputs/isabellesym.sty Tue Dec 29 22:03:02 2015 +0100
+++ b/lib/texinputs/isabellesym.sty Tue Dec 29 22:21:28 2015 +0100
@@ -157,22 +157,22 @@
\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
+\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath
+\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath
\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath
-\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
-\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
-\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath
\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath
\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb
-\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
-\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb
\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
+\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
-\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
\newcommand{\isasymmapsto}{\isamath{\mapsto}}
\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}