--- a/src/HOL/Reconstruction.thy Thu Oct 05 10:40:12 2006 +0200
+++ b/src/HOL/Reconstruction.thy Thu Oct 05 10:41:27 2006 +0200
@@ -54,6 +54,25 @@
lemma equal_imp_fequal: "X=Y ==> fequal X Y"
by (simp add: fequal_def)
+lemma COMBK1: "COMBK P == (%Q. P)"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBK_def)
+done
+
+lemma COMBI1: "COMBI == (%P. P)"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBI_def)
+done
+
+lemma COMBB1: "COMBB P Q == %R. P (Q R)"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBB_def)
+done
+
+
use "Tools/res_axioms.ML"
use "Tools/res_hol_clause.ML"
use "Tools/res_atp.ML"