added HOL/Tools/induct_tacs.ML;
authorwenzelm
Tue, 10 Jun 2008 19:15:20 +0200
changeset 27127 cd6617d57a16
parent 27126 3ede9103de8e
child 27128 d2374ba6c02e
added HOL/Tools/induct_tacs.ML;
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		\