src/HOL/Algebra/Sylow.thy

--- a/src/HOL/Algebra/Sylow.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -15,8 +15,8 @@
 subsection {*Order of a Group and Lagrange's Theorem*}
 
 constdefs
-  order     :: "(('a,'b) semigroup_scheme) => nat"
-   "order(S) == card(carrier S)"
+  order     :: "('a,'b) semigroup_scheme => nat"
+  "order S == card (carrier S)"
 
 theorem (in coset) lagrange:
      "[| finite(carrier G); subgroup H G |]