src/HOL/ex/ImperativeQuicksort.thy
2009-02-03 ago changed name space policy for Haskell includes
2009-01-08 ago split of Imperative_HOL theories from HOL-Library
2008-09-06 ago dropped "run" marker in monad syntax
2008-08-27 ago untabification
2008-07-30 ago SML_imp, OCaml_imp
2008-07-25 ago tuned
2008-07-21 ago added code generation
2008-07-19 ago added verification framework for the HeapMonad and quicksort as example for this framework