changeset 82663 | bd951e02d6b9 |
parent 81545 | 6f8a56a6b391 |
--- a/src/FOL/IFOL.thy Thu May 22 19:59:43 2025 +0200 +++ b/src/FOL/IFOL.thy Sat May 24 09:06:26 2025 +0200 @@ -9,6 +9,7 @@ abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1" begin +ML_file \<open>~~/src/Tools/simp_legacy.ML\<close> ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> ML_file \<open>~~/src/Provers/splitter.ML\<close> ML_file \<open>~~/src/Provers/hypsubst.ML\<close>