equal
deleted
inserted
replaced
11 "Tools/mirabelle_metis.ML" |
11 "Tools/mirabelle_metis.ML" |
12 "Tools/mirabelle_quickcheck.ML" |
12 "Tools/mirabelle_quickcheck.ML" |
13 "Tools/mirabelle_refute.ML" |
13 "Tools/mirabelle_refute.ML" |
14 "Tools/mirabelle_sledgehammer.ML" |
14 "Tools/mirabelle_sledgehammer.ML" |
15 "Tools/mirabelle_sledgehammer_filter.ML" |
15 "Tools/mirabelle_sledgehammer_filter.ML" |
16 "Tools/sledgehammer_tactic.ML" |
|
17 begin |
16 begin |
18 |
17 |
19 text {* |
18 text {* |
20 Only perform type-checking of the actions, |
19 Only perform type-checking of the actions, |
21 any reasonable test would be too complicated. |
20 any reasonable test would be too complicated. |