diff -r b503da67d2f7 -r 65a546c2b8ed ex/qsort.thy --- 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"