added verification framework for the HeapMonad and quicksort as example for this framework
(* Title: HOL/IMP/ROOT.ML
ID: $Id$
Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
Copyright 1995 TUM
Caveat: HOLCF/IMP depends on HOL/IMP
*)
use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler"];