--- a/doc-src/AxClass/Group/Semigroups.thy Sun May 21 14:49:28 2000 +0200
+++ b/doc-src/AxClass/Group/Semigroups.thy Sun May 21 21:48:39 2000 +0200
@@ -1,16 +1,8 @@
theory Semigroups = Main:;
-text {*
- \noindent Associativity of binary operations:
-*};
constdefs
is_assoc :: "('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> bool"
- "is_assoc f == \\<forall>x y z. f (f x y) z = f x (f y z)";
-
-text {*
- \medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}:
- %term (latex xsymbols symbols) "op \<Oplus>";
-*};
+ "is_assoc f \\<equiv> \\<forall>x y z. f (f x y) z = f x (f y z)";
consts
plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Oplus>" 65);
@@ -18,11 +10,6 @@
plus_semigroup < "term"
assoc: "is_assoc (op \<Oplus>)";
-text {*
- \medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}:
- %term (latex xsymbols symbols) "op \<Otimes>";
-*};
-
consts
times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Otimes>" 65);
axclass