src/HOL/Induct/ROOT.ML
changeset 15172 73069e033a0b
parent 14527 bc9e5587d05a
child 17598 7540ccd2b445
--- a/src/HOL/Induct/ROOT.ML	Thu Sep 02 14:50:00 2004 +0200
+++ b/src/HOL/Induct/ROOT.ML	Thu Sep 02 16:52:21 2004 +0200
@@ -1,6 +1,7 @@
 
 time_use_thy "Mutil";
 time_use_thy "QuoDataType";
+time_use_thy "QuoNestedDataType";
 time_use_thy "Term";
 time_use_thy "ABexp";
 time_use_thy "Tree";