| changeset 1151 | c820b3cc3df0 |
| parent 1131 | 8e81ad0c6f12 |
| child 1153 | 5c5daf97cf2d |
--- a/src/HOL/Lambda/Confluence.thy Wed Jun 21 15:14:58 1995 +0200 +++ b/src/HOL/Lambda/Confluence.thy Wed Jun 21 15:47:10 1995 +0200 @@ -26,6 +26,6 @@ "confluent2(R) == !x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R)" - Church_Rosser_def "Church_Rosser(R) == \ -\ !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)" + Church_Rosser_def "Church_Rosser(R) == + !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)" end