src/HOL/Mirabelle/MirabelleTest.thy
changeset 32546 d68b7c181211
parent 32545 8631b421ffc3
parent 32544 e129333b9df0
child 32548 b4119bbb2b79
--- a/src/HOL/Mirabelle/MirabelleTest.thy	Wed Sep 09 12:27:12 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: MirabelleTest.thy
-   Author: Sascha Boehme
-*)
-
-header {* Simple test theory for Mirabelle actions *}
-
-theory MirabelleTest
-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