--- a/ex/qsort.thy Mon Jan 24 16:00:37 1994 +0100
+++ b/ex/qsort.thy Mon Jan 24 16:03:03 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/ex/qsort.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1994 TU Muenchen
+
+Quicksort
+*)
+
Qsort = List +
consts
sorted :: "[['a,'a] => bool, 'a list] => bool"