src/HOL/Sledgehammer.thy
changeset 39894 35ae5cf8c96a
parent 39890 a1695e2169d0
child 39942 1ae333bfef14
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 30 00:29:37 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 30 18:59:37 2010 +0200
     1.3 @@ -60,6 +60,12 @@
     1.4  lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
     1.5  by auto
     1.6  
     1.7 +lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
     1.8 +unfolding skolem_def COMBK_def by (rule refl)
     1.9 +
    1.10 +lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
    1.11 +lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
    1.12 +
    1.13  text{*Theorems for translation to combinators*}
    1.14  
    1.15  lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"