diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Algebras.thy
--- a/src/HOL/Algebras.thy	Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Algebras.thy	Wed Feb 10 08:49:26 2010 +0100
@@ -103,10 +103,6 @@
 class times =
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
 
-class inverse =
-  fixes inverse :: "'a \<Rightarrow> 'a"
-    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
-
 class abs =
   fixes abs :: "'a \<Rightarrow> 'a"
 begin