--- a/src/HOL/ex/document/root.tex	Tue Apr 26 11:38:19 2016 +0200
+++ b/src/HOL/ex/document/root.tex	Tue Apr 26 11:56:06 2016 +0200
@@ -10,14 +10,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
-\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
-\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
-\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
-\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
-\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
-
-
 
 \begin{document}