--- a/src/HOL/Induct/PropLog.thy Sun Jun 01 17:45:43 2008 +0200
+++ b/src/HOL/Induct/PropLog.thy Mon Jun 02 13:21:06 2008 +0200
@@ -134,14 +134,13 @@
lemma false_imp: "H |- p->false ==> H |- p->q"
apply (rule deduction)
-apply (erule weaken_left_insert [THEN thms_notE])
-apply blast
+apply (metis H insert_iff weaken_left_insert thms_notE)
done
lemma imp_false:
"[| H |- p; H |- q->false |] ==> H |- (p->q)->false"
apply (rule deduction)
-apply (blast intro: weaken_left_insert thms.MP thms.H)
+apply (metis H MP insert_iff weaken_left_insert)
done
lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"