src/HOL/Lambda/ROOT.ML
author wenzelm
Sat, 02 Sep 2000 21:49:51 +0200
changeset 9803 bc883b390d91
parent 9115 67409447f788
child 10264 ef384b242d09
permissions -rw-r--r--
use Args.mode;

(*  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 "Type";