--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/Prefix.thy	Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,13 @@
+(*  Title: 	HOL/Lex/Prefix.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1995 TUM
+*)
+
+Prefix = List +
+
+arities list :: (term)ord
+
+defs
+	prefix_def     "xs <= zs  ==  ? ys. zs = xs@ys"
+end