1
(* Title: HOL/Lex/Prefix.thy
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1995 TUM
5
*)
6
7
Prefix = List +
8
9
arities list :: (term)ord
10
11
defs
12
prefix_def "xs <= zs == ? ys. zs = xs@ys"
13
end