| changeset 68816 | 5a53724fe247 |
| parent 63906 | fa799a8e4adc |
| child 69587 | 53982d5ec0bb |
--- a/src/FOL/IFOL.thy Mon Aug 27 14:31:52 2018 +0200 +++ b/src/FOL/IFOL.thy Mon Aug 27 14:42:24 2018 +0200 @@ -8,6 +8,7 @@ imports Pure begin +ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close> ML_file "~~/src/Tools/misc_legacy.ML" ML_file "~~/src/Provers/splitter.ML" ML_file "~~/src/Provers/hypsubst.ML"