added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
(* 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 "Compiler";