changeset 1476 | 608483c2122a |
parent 1344 | f172a7f14e49 |
child 6675 | 63e53327f5e5 |
--- a/src/HOL/Lex/Prefix.thy Mon Feb 05 21:27:16 1996 +0100 +++ b/src/HOL/Lex/Prefix.thy Mon Feb 05 21:29:06 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Lex/Prefix.thy +(* Title: HOL/Lex/Prefix.thy ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1995 TUM *) @@ -9,5 +9,5 @@ arities list :: (term)ord defs - prefix_def "xs <= zs == ? ys. zs = xs@ys" + prefix_def "xs <= zs == ? ys. zs = xs@ys" end