| changeset 74986 | fc664e4fbf6d |
| parent 74948 | 15ce207f69c8 |
| child 79941 | 6a3212bedfad |
--- a/src/HOL/Mirabelle.thy Mon Jan 17 17:04:50 2022 +0000 +++ b/src/HOL/Mirabelle.thy Tue Jan 18 17:55:20 2022 +0100 @@ -9,6 +9,7 @@ imports Sledgehammer Predicate_Compile Presburger begin +ML_file \<open>Tools/Mirabelle/mirabelle_util.ML\<close> ML_file \<open>Tools/Mirabelle/mirabelle.ML\<close> ML \<open>