changeset 25502 | 9200b36280c0 |
parent 25162 | ad4d5365d9d8 |
child 25571 | c9e39eafc7a0 |
--- a/src/HOL/Library/Parity.thy Thu Nov 29 07:55:46 2007 +0100 +++ b/src/HOL/Library/Parity.thy Thu Nov 29 17:08:26 2007 +0100 @@ -17,7 +17,7 @@ "odd x \<equiv> \<not> even x" instance int :: even_odd - even_def[presburger]: "even x \<equiv> x mod 2 = 0" .. + even_def[presburger]: "even x \<equiv> (x\<Colon>int) mod 2 = 0" .. instance nat :: even_odd even_nat_def[presburger]: "even x \<equiv> even (int x)" ..