diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/ex/ROOT.ML --- a/src/LK/ex/ROOT.ML Thu Oct 10 10:57:33 1996 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: LK/ex/ROOT - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Executes all examples for Classical Logic. -*) - -LK_build_completed; (*Cause examples to fail if LK did*) - -writeln"Root file for LK examples"; - -proof_timing := true; -time_use "ex/prop.ML"; -time_use "ex/quant.ML"; -time_use "ex/hardquant.ML"; - -maketest"END: Root file for LK examples";