| changeset 4502 | 337c073de95e |
| parent 2525 | 477c05586286 |
| child 5184 | 9b8547a9496a |
--- a/src/HOL/MiniML/Instance.thy Mon Dec 29 21:39:22 1997 +0100 +++ b/src/HOL/MiniML/Instance.thy Tue Dec 30 11:14:09 1997 +0100 @@ -44,6 +44,6 @@ instance list :: (ord)ord defs le_env_def - "A <= B == length B = length A & (!i. i < length A --> nth i A <= nth i B)" + "A <= B == length B = length A & (!i. i < length A --> A!i <= B!i)" end