changeset 73015 | 2d7060a3ea11 |
parent 71959 | ee2c7f0dd1be |
child 74300 | 33f13d2d211c |
--- a/src/FOL/FOL.thy Sun Dec 27 15:55:42 2020 +0100 +++ b/src/FOL/FOL.thy Sun Dec 27 17:53:08 2020 +0100 @@ -5,8 +5,8 @@ section \<open>Classical first-order logic\<close> theory FOL -imports IFOL -keywords "print_claset" "print_induct_rules" :: diag + imports IFOL + keywords "print_claset" "print_induct_rules" :: diag begin ML_file \<open>~~/src/Provers/classical.ML\<close>