--- a/src/HOL/Reconstruction.thy Fri Oct 06 11:17:27 2006 +0200
+++ b/src/HOL/Reconstruction.thy Fri Oct 06 11:17:53 2006 +0200
@@ -54,19 +54,19 @@
lemma equal_imp_fequal: "X=Y ==> fequal X Y"
by (simp add: fequal_def)
-lemma COMBK1: "COMBK P == (%Q. P)"
+lemma K_simp: "COMBK P == (%Q. P)"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBK_def)
done
-lemma COMBI1: "COMBI == (%P. P)"
+lemma I_simp: "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)"
+lemma B_simp: "COMBB P Q == %R. P (Q R)"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBB_def)