| changeset 275 | 34ad627ac5d5 |
| parent 274 | df225aa45770 |
| child 276 | 783d6c940e45 |
| 274:df225aa45770 | 275:34ad627ac5d5 |
|---|---|
37 "my_plus (x, y) (u, v) = (x + u, y + v)" |
37 "my_plus (x, y) (u, v) = (x + u, y + v)" |
38 |
38 |
39 quotient_def |
39 quotient_def |
40 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
40 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
41 where |
41 where |
42 "PLUS x y \<equiv> my_plus x y" |
42 "PLUS \<equiv> my_plus" |
43 |
43 |
44 term PLUS |
44 term PLUS |
45 thm PLUS_def |
45 thm PLUS_def |
46 |
46 |
47 fun |
47 fun |