src/HOL/Lambda/Commutation.thy
changeset 3439 54785105178c
parent 1476 608483c2122a
child 8624 69619f870939
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Mon Jun 16 14:25:33 1997 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Tue Jun 17 09:01:56 1997 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    diamond_def "diamond R   == commute R R"
     1.5  
     1.6    Church_Rosser_def "Church_Rosser(R) ==   
     1.7 -  !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
     1.8 +  !x y. (x,y) : (R Un R^-1)^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
     1.9  
    1.10  translations
    1.11    "confluent R" == "diamond(R^*)"