equal
deleted
inserted
replaced
121 (fn prems=> [rtac impI 1, eresolve_tac prems 1]); |
121 (fn prems=> [rtac impI 1, eresolve_tac prems 1]); |
122 |
122 |
123 qed_goalw "notE" HOL.thy [not_def] "[| ~P; P |] ==> R" |
123 qed_goalw "notE" HOL.thy [not_def] "[| ~P; P |] ==> R" |
124 (fn prems => [rtac (prems MRS mp RS FalseE) 1]); |
124 (fn prems => [rtac (prems MRS mp RS FalseE) 1]); |
125 |
125 |
|
126 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R" |
|
127 (fn _ => [REPEAT (ares_tac [notE] 1)]); |
|
128 |
126 |
129 |
127 (** Implication **) |
130 (** Implication **) |
128 section "-->"; |
131 section "-->"; |
129 |
132 |
130 qed_goal "impE" HOL.thy "[| P-->Q; P; Q ==> R |] ==> R" |
133 qed_goal "impE" HOL.thy "[| P-->Q; P; Q ==> R |] ==> R" |