removed foo_build_completed -- now handled by session management (via usedir);
(* Title: LCF/ex/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1991 University of CambridgeSome examples from Lawrence Paulson's book Logic and Computation.*)writeln"Root file for LCF examples";set proof_timing;use_thy "Ex1";use_thy "Ex2";use_thy "Ex3";use_thy "Ex4";