| changeset 1476 | 608483c2122a |
| parent 1344 | f172a7f14e49 |
| child 6675 | 63e53327f5e5 |
| 1475:7f5a4cd08209 | 1476:608483c2122a |
|---|---|
1 (* Title: HOL/Lex/Prefix.thy |
1 (* Title: HOL/Lex/Prefix.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 *) |
5 *) |
6 |
6 |
7 Prefix = List + |
7 Prefix = List + |
8 |
8 |
9 arities list :: (term)ord |
9 arities list :: (term)ord |
10 |
10 |
11 defs |
11 defs |
12 prefix_def "xs <= zs == ? ys. zs = xs@ys" |
12 prefix_def "xs <= zs == ? ys. zs = xs@ys" |
13 end |
13 end |