1
(* Title: HOL/IMP/ROOT.ML
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1998 TUM
5
*)
6
7
time_use_thy "Examples";