equal
deleted
inserted
replaced
58 by (simp add: fequal_def) |
58 by (simp add: fequal_def) |
59 |
59 |
60 lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" |
60 lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" |
61 by auto |
61 by auto |
62 |
62 |
|
63 lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))" |
|
64 unfolding skolem_def COMBK_def by (rule refl) |
|
65 |
|
66 lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] |
|
67 lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] |
|
68 |
63 text{*Theorems for translation to combinators*} |
69 text{*Theorems for translation to combinators*} |
64 |
70 |
65 lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" |
71 lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" |
66 apply (rule eq_reflection) |
72 apply (rule eq_reflection) |
67 apply (rule ext) |
73 apply (rule ext) |