--- a/src/HOL/ex/Locales.thy Tue Dec 04 02:01:31 2001 +0100
+++ b/src/HOL/ex/Locales.thy Tue Dec 04 02:01:49 2001 +0100
@@ -25,7 +25,6 @@
text_raw {*
\newcommand{\isasyminv}{\isasyminverse}
- \newcommand{\isasymone}{\isamath{1}}
\newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
*}