(* Title: HOL/Lambda/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1995 TUM *) HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/Lambda"; loadpath := [".","Lambda"]; time_use_thy "Eta"; make_chart (); (*make HTML chart*)