# HG changeset patch
# User paulson
# Date 1160037687 -7200
# Node ID 1059f2316f8807b9fbf674907899e6ddaab2dc03
# Parent  fd0e33caeb3bf47f14104233962dfcea92c5bbfd
facts about combinators

diff -r fd0e33caeb3b -r 1059f2316f88 src/HOL/Reconstruction.thy
--- 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"