equal
deleted
inserted
replaced
470 |
470 |
471 (* quantifier instantiation *) |
471 (* quantifier instantiation *) |
472 |
472 |
473 val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast} |
473 val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast} |
474 |
474 |
475 fun quant_inst ctxt _ t = prove ctxt t (fn _ => |
475 fun quant_inst ctxt _ t = prove ctxt t (fn _ => |
476 REPEAT_ALL_NEW (rtac quant_inst_rule) |
476 REPEAT_ALL_NEW (rtac quant_inst_rule) |
477 THEN' rtac @{thm excluded_middle}) |
477 THEN' rtac @{thm excluded_middle}) |
478 |
478 |
479 |
479 |
480 (* propositional lemma *) |
480 (* propositional lemma *) |