src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 36098 53992c639da5
parent 35041 6eb917794a5c
child 37719 271ecd4fb9f9
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Apr 07 22:22:49 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Apr 08 08:17:27 2010 +0200
     1.3 @@ -1,4 +1,8 @@
     1.4 -(* Author: Lukas Bulwahn, TU Muenchen *)
     1.5 +(*  Title:      HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
     1.6 +    Author:     Lukas Bulwahn, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* An imperative implementation of Quicksort on arrays *}
    1.10  
    1.11  theory Imperative_Quicksort
    1.12  imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat