changeset 73015 | 2d7060a3ea11 |
parent 71959 | ee2c7f0dd1be |
child 74342 | 5d411d85da8c |
--- a/src/FOL/IFOL.thy Sun Dec 27 15:55:42 2020 +0100 +++ b/src/FOL/IFOL.thy Sun Dec 27 17:53:08 2020 +0100 @@ -6,8 +6,7 @@ theory IFOL imports Pure -abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1" - + abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1" begin ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>