--- a/src/HOL/Sledgehammer.thy Thu Sep 30 00:29:37 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Sep 30 18:59:37 2010 +0200
@@ -60,6 +60,12 @@
lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
by auto
+lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
+unfolding skolem_def COMBK_def by (rule refl)
+
+lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
+lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
+
text{*Theorems for translation to combinators*}
lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"