# HG changeset patch
# User paulson
# Date 1160126273 -7200
# Node ID 5abf3cd34a35596abb459fbe2b9cdaa75458947e
# Parent  724ab9896068bc4229f28793e8f7170d26a88c2b
renamed the combinator laws

diff -r 724ab9896068 -r 5abf3cd34a35 src/HOL/Reconstruction.thy
--- 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)