# HG changeset patch
# User haftmann
# Date 1414068231 -7200
# Node ID 1b2e7b78a3374d470df5f69516da8b35fd2dfc9b
# Parent  1df01f0c05895c80bb8af58630c3f71184383eb3
explicit definition restores HOL Light import after cb9d84d3e7f2

diff -r 1df01f0c0589 -r 1b2e7b78a337 src/HOL/Import/HOL_Light_Maps.thy
--- 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))"