# HG changeset patch
# User wenzelm
# Date 1213118120 -7200
# Node ID cd6617d57a1660307cff2c4d26a14c7b5fb9d0b3
# Parent  3ede9103de8e32d8d5306d762a43a25b5b2bacf1
added HOL/Tools/induct_tacs.ML;

diff -r 3ede9103de8e -r cd6617d57a16 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jun 10 19:15:19 2008 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 10 19:15:20 2008 +0200
@@ -129,7 +129,7 @@
   Tools/function_package/measure_functions.ML	\
   Tools/function_package/mutual.ML					\
   Tools/function_package/pattern_split.ML	\
-  Tools/function_package/size.ML Tools/inductive_codegen.ML	\
+  Tools/function_package/size.ML Tools/induct_tacs.ML Tools/inductive_codegen.ML	\
   Tools/inductive_package.ML Tools/inductive_realizer.ML		\
   Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML	\
   Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\