| changeset 12955 | f4d60f358cb6 |
| parent 12937 | 0c4fd7529467 |
| child 12965 | c8a97eb1e3c7 |
--- 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)+