changeset 516 | 1957113f0d7d |
parent 55 | 331d93292ee0 |
child 744 | 2054fa3c8d76 |
--- a/src/ZF/QPair.ML Fri Aug 12 12:28:46 1994 +0200 +++ b/src/ZF/QPair.ML Fri Aug 12 12:51:34 1994 +0200 @@ -208,8 +208,8 @@ val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE); val qsum_cs = - ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl] - addSDs [QInl_inject,QInr_inject]; + qpair_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl] + addSDs [QInl_inject,QInr_inject]; goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A"; by (fast_tac qsum_cs 1);