changeset 35084 | e25eedfc15ce |
parent 35026 | 02850d0b95ac |
child 35092 | cfe605c54e50 |
--- 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