equal
deleted
inserted
replaced
38 where |
38 where |
39 "PLUS \<equiv> my_plus" |
39 "PLUS \<equiv> my_plus" |
40 |
40 |
41 term PLUS |
41 term PLUS |
42 thm PLUS_def |
42 thm PLUS_def |
|
43 |
|
44 definition |
|
45 "MPLUS x y \<equiv> my_plus x y" |
|
46 |
|
47 term MPLUS |
|
48 thm MPLUS_def |
|
49 thm MPLUS_def_raw |
|
50 |
43 |
51 |
44 fun |
52 fun |
45 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
53 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
46 where |
54 where |
47 "my_neg (x, y) = (y, x)" |
55 "my_neg (x, y) = (y, x)" |