--- a/src/HOL/ex/Classpackage.thy Thu Sep 20 16:37:28 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy Thu Sep 20 16:37:29 2007 +0200
@@ -81,8 +81,6 @@
units :: "'a set" where
"units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
-end context monoid begin
-
lemma inv_obtain:
assumes "x \<in> units"
obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
@@ -120,8 +118,6 @@
"npow 0 x = \<^loc>\<one>"
| "npow (Suc n) x = x \<^loc>\<otimes> npow n x"
-end context monoid begin
-
abbreviation
npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
"x \<^loc>\<up> n \<equiv> npow n x"