src/HOL/Induct/ROOT.ML
changeset 6349 f7750d816c21
parent 5739 f35761a1e1c4
child 7019 71f2155cdd85
equal deleted inserted replaced
6348:fdcbeaddd5fc 6349:f7750d816c21
     4     Copyright   1997  University of Cambridge
     4     Copyright   1997  University of Cambridge
     5 
     5 
     6 Examples of Inductive and Coinductive Definitions
     6 Examples of Inductive and Coinductive Definitions
     7 *)
     7 *)
     8 
     8 
     9 HOL_build_completed;    (*Make examples fail if HOL did*)
     9 writeln"Root file for HOL/Induct";
    10 
    10 
    11 writeln"Root file for HOL/Induct";
       
    12 set proof_timing;
    11 set proof_timing;
    13 time_use_thy "Perm";
    12 time_use_thy "Perm";
    14 time_use_thy "Comb";
    13 time_use_thy "Comb";
    15 time_use_thy "Mutil";
    14 time_use_thy "Mutil";
    16 time_use_thy "Acc";
    15 time_use_thy "Acc";