src/HOL/Induct/ROOT.ML
changeset 9000 c20d58286a51
parent 8917 2ff6f8693c4f
child 9450 c97dba47e504
equal deleted inserted replaced
8999:ad8260dc6e4a 9000:c20d58286a51
     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 writeln"Root file for HOL/Induct";
       
    10 
       
    11 set proof_timing;
       
    12 time_use_thy "Perm";
     9 time_use_thy "Perm";
    13 time_use_thy "Comb";
    10 time_use_thy "Comb";
    14 time_use_thy "Mutil";
    11 time_use_thy "Mutil";
    15 time_use_thy "Acc";
    12 time_use_thy "Acc";
    16 time_use_thy "MultisetOrder";
    13 time_use_thy "MultisetOrder";