src/Sequents/LK/ROOT.ML
changeset 6252 935f183bf406
child 6349 f7750d816c21
equal deleted inserted replaced
6251:4d89d4f0ab17 6252:935f183bf406
       
     1 (*  Title:      LK/ex/ROOT
       
     2     ID:         $Id$
       
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
       
     4     Copyright   1992  University of Cambridge
       
     5 
       
     6 Executes all examples for Classical Logic. 
       
     7 *)
       
     8 
       
     9 Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
       
    10 
       
    11 writeln"Root file for LK examples";
       
    12 
       
    13 set proof_timing;
       
    14 time_use "prop.ML";
       
    15 time_use "quant.ML";
       
    16 time_use "hardquant.ML";