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