src/HOL/Import/HOL_Light_Maps.thy
changeset 58773 1b2e7b78a337
parent 56266 da5f22a60cb3
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Thu Oct 23 14:43:48 2014 +0200
     1.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Thu Oct 23 14:43:51 2014 +0200
     1.3 @@ -181,9 +181,13 @@
     1.4    "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
     1.5    by (auto simp add: min.absorb_iff1 fun_eq_iff)
     1.6  
     1.7 +definition even
     1.8 +where
     1.9 +  "even = Parity.even"
    1.10 +  
    1.11  lemma EVEN[import_const "EVEN" : even]:
    1.12    "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
    1.13 -  by simp
    1.14 +  by (simp add: even_def)
    1.15  
    1.16  lemma SUB[import_const "-" : minus]:
    1.17    "(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"