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