--- a/src/HOL/ex/Locales.thy Wed Feb 27 18:41:28 2002 +0100
+++ b/src/HOL/ex/Locales.thy Wed Feb 27 19:43:20 2002 +0100
@@ -11,7 +11,7 @@
text_raw {*
\newcommand{\isasyminv}{\isasyminverse}
\newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
- \newcommand{\isasymUSES}{\isatext{\isakeyword{uses}}}
+ \newcommand{\isasymINCLUDES}{\isatext{\isakeyword{includes}}}
*}
subsection {* Overview *}
@@ -199,7 +199,7 @@
definition of @{text abelian_group} is actually evaluated
dynamically. Thus any results in @{text group} are made available
to the derived context of @{text abelian_group} as well. Note that
- the alternative context element @{text \<USES>} would import
+ the alternative context element @{text \<INCLUDES>} would import
existing locales in a static fashion, without participating in
further facts emerging later on.