renamed the combinator laws
authorpaulson
Fri Oct 06 11:17:53 2006 +0200 (2006-10-06)
changeset 208695abf3cd34a35
parent 20868 724ab9896068
child 20870 992bcbff055a
renamed the combinator laws
src/HOL/Reconstruction.thy
     1.1 --- a/src/HOL/Reconstruction.thy	Fri Oct 06 11:17:27 2006 +0200
     1.2 +++ b/src/HOL/Reconstruction.thy	Fri Oct 06 11:17:53 2006 +0200
     1.3 @@ -54,19 +54,19 @@
     1.4  lemma equal_imp_fequal: "X=Y ==> fequal X Y"
     1.5    by (simp add: fequal_def)
     1.6  
     1.7 -lemma COMBK1: "COMBK P == (%Q. P)"
     1.8 +lemma K_simp: "COMBK P == (%Q. P)"
     1.9  apply (rule eq_reflection) 
    1.10  apply (rule ext) 
    1.11  apply (simp add: COMBK_def) 
    1.12  done
    1.13  
    1.14 -lemma COMBI1: "COMBI == (%P. P)"
    1.15 +lemma I_simp: "COMBI == (%P. P)"
    1.16  apply (rule eq_reflection) 
    1.17  apply (rule ext) 
    1.18  apply (simp add: COMBI_def) 
    1.19  done
    1.20  
    1.21 -lemma COMBB1: "COMBB P Q == %R. P (Q R)"
    1.22 +lemma B_simp: "COMBB P Q == %R. P (Q R)"
    1.23  apply (rule eq_reflection) 
    1.24  apply (rule ext) 
    1.25  apply (simp add: COMBB_def)