equal
deleted
inserted
replaced
14 |
14 |
15 abbreviation |
15 abbreviation |
16 odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where |
16 odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where |
17 "odd x \<equiv> \<not> even x" |
17 "odd x \<equiv> \<not> even x" |
18 |
18 |
19 instantiation int :: even_odd |
19 instantiation nat and int :: even_odd |
20 begin |
20 begin |
21 |
21 |
22 definition |
22 definition |
23 even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0" |
23 even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0" |
24 |
|
25 instance .. |
|
26 |
|
27 end |
|
28 |
|
29 instantiation nat :: even_odd |
|
30 begin |
|
31 |
24 |
32 definition |
25 definition |
33 even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)" |
26 even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)" |
34 |
27 |
35 instance .. |
28 instance .. |