changeset 81254 | d3c0734059ee |
parent 78728 | 72631efa3821 |
--- a/src/HOL/Metis.thy Thu Oct 24 22:05:57 2024 +0200 +++ b/src/HOL/Metis.thy Fri Oct 25 15:31:58 2024 +0200 @@ -44,6 +44,7 @@ ML_file \<open>Tools/Metis/metis_generate.ML\<close> ML_file \<open>Tools/Metis/metis_reconstruct.ML\<close> +ML_file \<open>Tools/Metis/metis_instantiations.ML\<close> ML_file \<open>Tools/Metis/metis_tactic.ML\<close> hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda