--- a/src/FOL/IsaMakefile Tue Apr 08 20:09:54 2008 +0200
+++ b/src/FOL/IsaMakefile Tue Apr 08 20:14:36 2008 +0200
@@ -35,7 +35,7 @@
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/rw_inst.ML \
$(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
- $(SRC)/Tools/induct.ML \
+ $(SRC)/Tools/induct.ML $(SRC)/Tools/atomize_elim.ML \
$(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML \
document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
--- a/src/HOL/IsaMakefile Tue Apr 08 20:09:54 2008 +0200
+++ b/src/HOL/IsaMakefile Tue Apr 08 20:14:36 2008 +0200
@@ -90,7 +90,7 @@
$(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML \
$(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML \
$(SRC)/Tools/code/code_package.ML $(SRC)/Tools/code/code_target.ML \
- $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML \
+ $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \
$(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \
Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy \
Divides.thy Equiv_Relations.thy Extraction.thy \