changeset 1465 | 5d7a7e439cec |
parent 1266 | 3ae9fe3c0f68 |
child 1750 | 817a34a54fb0 |
--- a/src/HOL/ex/InSort.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/InSort.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/insort.ML +(* Title: HOL/ex/insort.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1994 TU Muenchen Correctness proof of insertion sort.