equal
deleted
inserted
replaced
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 instance int :: even_odd |
19 instance int :: even_odd |
20 even_def[presburger]: "even x \<equiv> x mod 2 = 0" .. |
20 even_def[presburger]: "even x \<equiv> (x\<Colon>int) mod 2 = 0" .. |
21 |
21 |
22 instance nat :: even_odd |
22 instance nat :: even_odd |
23 even_nat_def[presburger]: "even x \<equiv> even (int x)" .. |
23 even_nat_def[presburger]: "even x \<equiv> even (int x)" .. |
24 |
24 |
25 |
25 |