equal
deleted
inserted
replaced
21 "ZERO \<equiv> (0::nat, 0::nat)" |
21 "ZERO \<equiv> (0::nat, 0::nat)" |
22 |
22 |
23 term ZERO |
23 term ZERO |
24 thm ZERO_def |
24 thm ZERO_def |
25 |
25 |
|
26 ML {* prop_of @{thm ZERO_def} *} |
|
27 |
26 quotient_def |
28 quotient_def |
27 ONE::"my_int" |
29 ONE::"my_int" |
28 where |
30 where |
29 "ONE \<equiv> (1::nat, 0::nat)" |
31 "ONE \<equiv> (1::nat, 0::nat)" |
30 |
32 |
41 where |
43 where |
42 "PLUS \<equiv> my_plus" |
44 "PLUS \<equiv> my_plus" |
43 |
45 |
44 term PLUS |
46 term PLUS |
45 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} *} |
46 |
52 |
47 fun |
53 fun |
48 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
54 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
49 where |
55 where |
50 "my_neg (x, y) = (y, x)" |
56 "my_neg (x, y) = (y, x)" |