changeset 1156 | b373cb33352f |
parent 1153 | 5c5daf97cf2d |
--- a/src/HOL/Lambda/Confluence.thy Thu Jun 22 17:13:05 1995 +0200 +++ b/src/HOL/Lambda/Confluence.thy Fri Jun 23 09:15:09 1995 +0200 @@ -14,7 +14,7 @@ defs diamond_def - "diamond(R) == !x y z. (x,y):R --> (x,z):R --> (EX u. (y,u):R & (z,u):R)" + "diamond(R) == !x y.(x,y):R --> (!z.(x,z):R --> (EX u. (y,u):R & (z,u):R))" confluent_def "confluent(R) == diamond(R^*)"