equal
deleted
inserted
replaced
6 |
6 |
7 theory Mirabelle_Test |
7 theory Mirabelle_Test |
8 imports Main Mirabelle |
8 imports Main Mirabelle |
9 begin |
9 begin |
10 |
10 |
11 ML_file "Tools/mirabelle_arith.ML" |
11 ML_file \<open>Tools/mirabelle_arith.ML\<close> |
12 ML_file "Tools/mirabelle_metis.ML" |
12 ML_file \<open>Tools/mirabelle_metis.ML\<close> |
13 ML_file "Tools/mirabelle_quickcheck.ML" |
13 ML_file \<open>Tools/mirabelle_quickcheck.ML\<close> |
14 ML_file "Tools/mirabelle_refute.ML" |
14 ML_file \<open>Tools/mirabelle_refute.ML\<close> |
15 ML_file "Tools/mirabelle_sledgehammer.ML" |
15 ML_file \<open>Tools/mirabelle_sledgehammer.ML\<close> |
16 ML_file "Tools/mirabelle_sledgehammer_filter.ML" |
16 ML_file \<open>Tools/mirabelle_sledgehammer_filter.ML\<close> |
17 ML_file "Tools/mirabelle_try0.ML" |
17 ML_file \<open>Tools/mirabelle_try0.ML\<close> |
18 |
18 |
19 text \<open> |
19 text \<open> |
20 Only perform type-checking of the actions, |
20 Only perform type-checking of the actions, |
21 any reasonable test would be too complicated. |
21 any reasonable test would be too complicated. |
22 \<close> |
22 \<close> |