--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Wed Aug 22 22:55:41 2012 +0200
@@ -6,16 +6,16 @@
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"
- "Tools/mirabelle_sledgehammer_filter.ML"
- "Tools/mirabelle_try0.ML"
begin
+ML_file "Tools/mirabelle_arith.ML"
+ML_file "Tools/mirabelle_metis.ML"
+ML_file "Tools/mirabelle_quickcheck.ML"
+ML_file "Tools/mirabelle_refute.ML"
+ML_file "Tools/mirabelle_sledgehammer.ML"
+ML_file "Tools/mirabelle_sledgehammer_filter.ML"
+ML_file "Tools/mirabelle_try0.ML"
+
text {*
Only perform type-checking of the actions,
any reasonable test would be too complicated.