# HG changeset patch # User krauss # Date 1300713959 -3600 # Node ID a14e9cf805e00058a5911d881ccaed5241163787 # Parent fb155c75072d056618edb1bcf84e873621cfefc9 more precise dependencies diff -r fb155c75072d -r a14e9cf805e0 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Mar 21 12:43:26 2011 +0100 +++ b/src/HOL/IsaMakefile Mon Mar 21 14:25:59 2011 +0100 @@ -1315,7 +1315,8 @@ Mirabelle/Tools/mirabelle_refute.ML \ Mirabelle/Tools/mirabelle_sledgehammer.ML \ Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \ - Mirabelle/Tools/sledgehammer_tactics.ML \ + Mirabelle/Tools/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