src/FOL/ex/ROOT.ML
changeset 9000 c20d58286a51
parent 8909 96503b90307b
child 9205 f171fa6a0989
equal deleted inserted replaced
8999:ad8260dc6e4a 9000:c20d58286a51
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Executes all examples for First-Order Logic. 
     6 Executes all examples for First-Order Logic. 
     7 *)
     7 *)
     8 
       
     9 writeln"Root file for FOL examples";
       
    10 
       
    11 set proof_timing;
       
    12 
     8 
    13 time_use     "intro.ML";
     9 time_use     "intro.ML";
    14 time_use_thy "Nat";
    10 time_use_thy "Nat";
    15 time_use     "foundn.ML";
    11 time_use     "foundn.ML";
    16 time_use_thy "Prolog";
    12 time_use_thy "Prolog";