added type global_theory -- theory or local_theory;
added begin/exit_local_theory;
removed theory_context;
renamed body_context_node to presentation_context;
removed copy (checkpoint twice instead -- avoids unrelated theories);
(* 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
*)
time_use_thy "Expr";
time_use_thy "Transition";
time_use_thy "VC";
time_use_thy "Examples";
time_use_thy "Compiler0";
time_use_thy "Compiler";