(* Title: HOL/Lambda/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM *) time_use_thy "Eta"; with_path "../Induct" time_use_thy "Acc"; time_use_thy "InductTermi";