# HG changeset patch
# User paulson
# Date 1081421363 -7200
# Node ID 716c9def561470aeed270fed30d79d4081c09bd6
# Parent  e94fd774ecf5257c9b89ffe2408845b8f4cd4a49
new theory

diff -r e94fd774ecf5 -r 716c9def5614 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Apr 08 12:45:22 2004 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 08 12:49:23 2004 +0200
@@ -208,7 +208,7 @@
 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
   Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
-  Induct/PropLog.thy Induct/ROOT.ML \
+  Induct/PropLog.thy Induct/QuoDataType.thy Induct/ROOT.ML \
   Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   Induct/Tree.thy Induct/document/root.tex