ex/qsort.ML

--- a/ex/qsort.ML	Mon Jan 24 16:00:37 1994 +0100
+++ b/ex/qsort.ML	Mon Jan 24 16:03:03 1994 +0100
@@ -1,3 +1,11 @@
+(*  Title: 	HOL/ex/qsort.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+Two verifications of Quicksort
+*)
+
 val ss = list_ss addsimps
  [Qsort.mset_Nil,Qsort.mset_Cons,
   Qsort.sorted_Nil,Qsort.sorted_Cons,