equal
deleted
inserted
replaced
20 make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
20 make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
21 *} |
21 *} |
22 |
22 |
23 term ZERO |
23 term ZERO |
24 thm ZERO_def |
24 thm ZERO_def |
|
25 |
|
26 (* |
|
27 quotient_def (with my_int) |
|
28 ZERO :: "my_int" |
|
29 where |
|
30 "ZERO \<equiv> (0::nat, 0::nat)" |
|
31 *) |
25 |
32 |
26 local_setup {* |
33 local_setup {* |
27 make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
34 make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
28 *} |
35 *} |
29 |
36 |