equal
deleted
inserted
replaced
6 |
6 |
7 theory Classpackage |
7 theory Classpackage |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 class semigroup = |
11 class semigroup = type + |
12 fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70) |
12 fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70) |
13 assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)" |
13 assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)" |
14 |
14 |
15 instance nat :: semigroup |
15 instance nat :: semigroup |
16 "m \<otimes> n \<equiv> m + n" |
16 "m \<otimes> n \<equiv> m + n" |