--- a/src/HOL/ex/Locales.thy Tue Feb 26 21:44:06 2002 +0100
+++ b/src/HOL/ex/Locales.thy Tue Feb 26 21:44:29 2002 +0100
@@ -336,7 +336,8 @@
*}
lemma
- uses group G + group H
+ includes group G
+ includes group H
shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
"x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
"x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
--- a/src/Pure/Isar/outer_parse.ML Tue Feb 26 21:44:06 2002 +0100
+++ b/src/Pure/Isar/outer_parse.ML Tue Feb 26 21:44:29 2002 +0100
@@ -300,7 +300,7 @@
local
val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
-val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "uses";
+val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "includes";
fun plus1 scan =
scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
@@ -324,7 +324,7 @@
>> (Locale.Elem o Locale.Defines) ||
$$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
>> (Locale.Elem o Locale.Notes) ||
- $$$ "uses" |-- !!! locale_expr >> Locale.Expr);
+ $$$ "includes" |-- !!! locale_expr >> Locale.Expr);
end;