equal
deleted
inserted
replaced
19 structure Old_SMT_Normalize: OLD_SMT_NORMALIZE = |
19 structure Old_SMT_Normalize: OLD_SMT_NORMALIZE = |
20 struct |
20 struct |
21 |
21 |
22 fun drop_fact_warning ctxt = |
22 fun drop_fact_warning ctxt = |
23 Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o |
23 Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o |
24 Display.string_of_thm ctxt) |
24 Thm.string_of_thm ctxt) |
25 |
25 |
26 |
26 |
27 (* general theorem normalizations *) |
27 (* general theorem normalizations *) |
28 |
28 |
29 (** instantiate elimination rules **) |
29 (** instantiate elimination rules **) |