equal
deleted
inserted
replaced
18 quotient_def |
18 quotient_def |
19 ZERO::"my_int" |
19 ZERO::"my_int" |
20 where |
20 where |
21 "ZERO \<equiv> (0::nat, 0::nat)" |
21 "ZERO \<equiv> (0::nat, 0::nat)" |
22 |
22 |
|
23 ML {* print_qconstinfo @{context} *} |
|
24 |
|
25 |
23 term ZERO |
26 term ZERO |
24 thm ZERO_def |
27 thm ZERO_def |
25 |
28 |
26 ML {* prop_of @{thm ZERO_def} *} |
29 ML {* prop_of @{thm ZERO_def} *} |
27 |
30 |
|
31 ML {* separate *} |
|
32 |
28 quotient_def |
33 quotient_def |
29 ONE::"my_int" |
34 ONE::"my_int" |
30 where |
35 where |
31 "ONE \<equiv> (1::nat, 0::nat)" |
36 "ONE \<equiv> (1::nat, 0::nat)" |
|
37 |
|
38 ML {* print_qconstinfo @{context} *} |
32 |
39 |
33 term ONE |
40 term ONE |
34 thm ONE_def |
41 thm ONE_def |
35 |
42 |
36 fun |
43 fun |
41 quotient_def |
48 quotient_def |
42 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
49 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
43 where |
50 where |
44 "PLUS \<equiv> my_plus" |
51 "PLUS \<equiv> my_plus" |
45 |
52 |
|
53 term my_plus |
46 term PLUS |
54 term PLUS |
47 thm PLUS_def |
55 thm PLUS_def |
48 |
56 |
49 fun |
57 fun |
50 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
58 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |