Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
small test case for main mirabelle functionality, which easily breaks without noticing
authorkrauss
Mon, 21 Mar 2011 12:43:26 +0100
changeset 42035 fb155c75072d
parent 42034 a77df5241959
child 42036 a14e9cf805e0
small test case for main mirabelle functionality, which easily breaks without noticing
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/src/HOL/IsaMakefile	Mon Mar 21 12:43:25 2011 +0100
+++ b/src/HOL/IsaMakefile	Mon Mar 21 12:43:26 2011 +0100
@@ -1315,8 +1315,10 @@
   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 \
+  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
isabelle