--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Fri Sep 04 13:57:56 2009 +0200
@@ -0,0 +1,22 @@
+(* Title: Mirabelle_Test.thy
+ Author: Sascha Boehme
+*)
+
+header {* Simple test theory for Mirabelle actions *}
+
+theory Mirabelle_Test
+imports Main Mirabelle
+uses
+ "Tools/mirabelle_arith.ML"
+ "Tools/mirabelle_metis.ML"
+ "Tools/mirabelle_quickcheck.ML"
+ "Tools/mirabelle_refute.ML"
+ "Tools/mirabelle_sledgehammer.ML"
+begin
+
+(*
+ only perform type-checking of the actions,
+ any reasonable test would be too complicated
+*)
+
+end