--- a/src/HOL/Import/HOL_Light_Maps.thy Thu Oct 23 14:43:48 2014 +0200
+++ b/src/HOL/Import/HOL_Light_Maps.thy Thu Oct 23 14:43:51 2014 +0200
@@ -181,9 +181,13 @@
"min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
by (auto simp add: min.absorb_iff1 fun_eq_iff)
+definition even
+where
+ "even = Parity.even"
+
lemma EVEN[import_const "EVEN" : even]:
"even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
- by simp
+ by (simp add: even_def)
lemma SUB[import_const "-" : minus]:
"(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"