src/HOL/ex/Locales.thy

--- a/src/HOL/ex/Locales.thy	Fri Oct 31 06:54:22 2003 +0100
+++ b/src/HOL/ex/Locales.thy	Thu Nov 06 14:18:05 2003 +0100
@@ -321,6 +321,9 @@
   assumes left_inv: "x\<inv> \<cdot> x = \<one>"
     and left_one: "\<one> \<cdot> x = x"
 
+declare semigroup.intro [intro?]
+  group.intro [intro?] group_axioms.intro [intro?]
+
 text {*
   Note that we prefer to call the @{text group} record structure
   @{text G} rather than @{text S} inherited from @{text semigroup}.