src/HOL/Induct/ROOT.ML
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 17598 7540ccd2b445
child 23746 a455e69c31cc
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 
     2 (* $Id$ *)
     3 
     4 time_use_thy "Mutil";
     5 time_use_thy "QuoDataType";
     6 time_use_thy "QuoNestedDataType";
     7 time_use_thy "Term";
     8 time_use_thy "ABexp";
     9 time_use_thy "Tree";
    10 time_use_thy "Ordinals";
    11 time_use_thy "Sigma_Algebra";
    12 time_use_thy "Comb";
    13 time_use_thy "PropLog";
    14 time_use_thy "SList";
    15 time_use_thy "LFilter";