--- a/src/HOL/AxClasses/Tutorial/Semigroups.thy Sun Sep 17 22:15:08 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/Semigroups.thy Sun Sep 17 22:19:02 2000 +0200
@@ -3,18 +3,18 @@
Author: Markus Wenzel, TU Muenchen
*)
-theory Semigroups = Main:;
+theory Semigroups = Main:
consts
- times :: "'a => 'a => 'a" (infixl "[*]" 70);
+ times :: "'a => 'a => 'a" (infixl "[*]" 70)
axclass
semigroup < "term"
- assoc: "(x [*] y) [*] z = x [*] (y [*] z)";
+ assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
consts
- plus :: "'a => 'a => 'a" (infixl "[+]" 70);
+ plus :: "'a => 'a => 'a" (infixl "[+]" 70)
axclass
plus_semigroup < "term"
- assoc: "(x [+] y) [+] z = x [+] (y [+] z)";
+ assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
-end;
+end