equal
deleted
inserted
replaced
43 where |
43 where |
44 "PLUS \<equiv> my_plus" |
44 "PLUS \<equiv> my_plus" |
45 |
45 |
46 term PLUS |
46 term PLUS |
47 thm PLUS_def |
47 thm PLUS_def |
48 |
|
49 ML {* toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy"; *} |
|
50 |
|
51 ML {* prop_of @{thm PLUS_def} *} |
|
52 |
48 |
53 fun |
49 fun |
54 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
50 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
55 where |
51 where |
56 "my_neg (x, y) = (y, x)" |
52 "my_neg (x, y) = (y, x)" |