src/HOL/IsaMakefile

   Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
   Library/Reflection.thy Library/SML_Quickcheck.thy 			\
   Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
   Library/Sum_of_Squares/sos_wrapper.ML					\
   Library/Sum_of_Squares/sum_of_squares.ML				\
-  Library/TPTP.thy Library/Transitive_Closure_Table.thy			\
-  Library/Univ_Poly.thy Library/While_Combinator.thy Library/Zorn.thy	\
+  Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
+  Library/While_Combinator.thy Library/Zorn.thy	\
   $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
   Library/reflection.ML Library/reify_data.ML				\
   Library/Quickcheck_Narrowing.thy \
   Tools/Quickcheck/narrowing_generators.ML \
   Tools/Quickcheck/Narrowing_Engine.hs \

   ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
   ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
   ex/Quickcheck_Narrowing_Examples.thy \
   ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
   ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy	\
-  ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy	\
+  ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy			\
+  ex/sledgehammer_tactics.ML ex/Sqrt.thy				\
   ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy	\
-  ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy			\
+  ex/TPTP.thy ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy	\
   ex/While_Combinator_Example.thy ex/document/root.bib			\
   ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy	\
   ../Tools/interpretation_with_defs.ML
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 

   Mirabelle/Tools/mirabelle_metis.ML					\
   Mirabelle/Tools/mirabelle_quickcheck.ML				\
   Mirabelle/Tools/mirabelle_refute.ML					\
   Mirabelle/Tools/mirabelle_sledgehammer.ML 				\
   Mirabelle/Tools/mirabelle_sledgehammer_filter.ML			\
-  Mirabelle/Tools/sledgehammer_tactics.ML 				\
-  Mirabelle/lib/Tools/mirabelle Mirabelle/lib/scripts/mirabelle.pl	\
-  Library/FrechetDeriv.thy Library/Inner_Product.thy
+  ex/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle		\
+  Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy		\
+  Library/Inner_Product.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
 	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
 
 
 ## HOL-Word-SMT_Examples