# HG changeset patch
# User wenzelm
# Date 1007427709 -3600
# Node ID ce0961b1f5362b17c9995143b3eb8ccb1d50e74b
# Parent  c8d3c3d090808fea4cd6abd6a75f7810779d5ada
removed \newcommand{\isasymone};

diff -r c8d3c3d09080 -r ce0961b1f536 src/HOL/ex/Locales.thy
--- 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}}}
 *}