changeset 26411 | cd74690f3bfb |
parent 26286 | 3ff5d257f175 |
child 26496 | 49ae9456eba9 |
--- a/src/FOL/FOL.thy Wed Mar 26 22:39:58 2008 +0100 +++ b/src/FOL/FOL.thy Wed Mar 26 22:40:01 2008 +0100 @@ -163,6 +163,12 @@ qed qed +lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R" + by (rule classical) iprover + +lemma swap: "~ P ==> (~ R ==> P) ==> R" + by (rule classical) iprover + use "cladata.ML" setup Cla.setup setup cla_setup