[isabelle] Destruction rule setup



Some of the destruction rules in Isar are set up with [dest]; for example:
lemma impD [dest]: (A --> B) ==> A ==> B
lemma allD [dest]: (\forall x: B x) ==> B a
Others are not set up with [dest]; for example:
lemma not_conjD: ~(P & Q) ==> ~P | ~Q
lemma imp_to_disjD: P --> Q ==> ~P | Q
Why is this? Thanks! -WDMaurer

--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.