diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Sorting.ML --- a/src/HOL/ex/Sorting.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/Sorting.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/sorting.ML +(* Title: HOL/ex/sorting.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1994 TU Muenchen Some general lemmas