src/FOL/IsaMakefile
changeset 42793 88bee9f6eec7
parent 42138 e54a985daa61
child 42799 4e33894aec6d
--- a/src/FOL/IsaMakefile	Fri May 13 16:03:03 2011 +0200
+++ b/src/FOL/IsaMakefile	Fri May 13 22:55:00 2011 +0200
@@ -29,14 +29,13 @@
 
 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
-  $(SRC)/Tools/case_product.ML						\
-  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML	\
-  $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
+  $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML	\
+  $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML	\
   $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
   $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
   $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
   $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
-  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML cladata.ML	\
+  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\
   document/root.tex fologic.ML hypsubstdata.ML intprover.ML		\
   simpdata.ML
 	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL