1
(* Title: HOLCF/IMP/ROOT.ML
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1997 TU Muenchen
5
*)
6
7
add_path "../../HOL/IMP";
8
use_thy "Natural";
9
10
reset_path ();
11
use_thy "HoareEx";