1
(* Title: HOLCF/IMP/ROOT.ML
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1997 TU Muenchen
5
*)
6
7
with_path "../../HOL/IMP" time_use_thy "HoareEx";