| changeset 6675 | 63e53327f5e5 |
| parent 1476 | 608483c2122a |
| child 8523 | 7ffc94f2f42d |
--- a/src/HOL/Lex/Prefix.thy Fri May 21 10:47:07 1999 +0200 +++ b/src/HOL/Lex/Prefix.thy Fri May 21 10:50:04 1999 +0200 @@ -9,5 +9,8 @@ arities list :: (term)ord defs - prefix_def "xs <= zs == ? ys. zs = xs@ys" + prefix_def "xs <= zs == ? ys. zs = xs@ys" + + strict_prefix_def "xs < zs == xs <= zs & xs ~= (zs::'a list)" + end