equal
deleted
inserted
replaced
12 begin |
12 begin |
13 txt {* hypothetical group axiomatization *} |
13 txt {* hypothetical group axiomatization *} |
14 |
14 |
15 fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70) |
15 fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70) |
16 and one :: "'a" |
16 and one :: "'a" |
17 and inverse :: "'a => 'a" |
17 and inverse :: "'a \<Rightarrow> 'a" |
18 assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)" |
18 assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)" |
19 and left_one: "\<And>x. one ** x = x" |
19 and left_one: "\<And>x. one ** x = x" |
20 and left_inverse: "\<And>x. inverse x ** x = one" |
20 and left_inverse: "\<And>x. inverse x ** x = one" |
21 |
21 |
22 txt {* some consequences *} |
22 txt {* some consequences *} |