src/HOL/ex/ROOT.ML
changeset 6349 f7750d816c21
parent 5866 de6a1856c74a
child 7085 e5a5f8d23f26
equal deleted inserted replaced
6348:fdcbeaddd5fc 6349:f7750d816c21
     4     Copyright   1991  University of Cambridge
     4     Copyright   1991  University of Cambridge
     5 
     5 
     6 Executes miscellaneous examples for Higher-Order Logic. 
     6 Executes miscellaneous examples for Higher-Order Logic. 
     7 *)
     7 *)
     8 
     8 
     9 HOL_build_completed;    (*Cause examples to fail if HOL did*)
     9 writeln "Root file for HOL examples";
    10 
    10 
    11 writeln "Root file for HOL examples";
       
    12 set proof_timing;
    11 set proof_timing;
    13 
    12 
    14 (*some examples of recursive function definitions: the TFL package*)
    13 (*some examples of recursive function definitions: the TFL package*)
    15 time_use_thy "Recdefs";
    14 time_use_thy "Recdefs";
    16 time_use_thy "Primes";
    15 time_use_thy "Primes";