equal
deleted
inserted
replaced
206 val QInr_inject = standard (QInr_iff RS iffD1); |
206 val QInr_inject = standard (QInr_iff RS iffD1); |
207 val QInl_neq_QInr = standard (QInl_QInr_iff RS iffD1 RS FalseE); |
207 val QInl_neq_QInr = standard (QInl_QInr_iff RS iffD1 RS FalseE); |
208 val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE); |
208 val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE); |
209 |
209 |
210 val qsum_cs = |
210 val qsum_cs = |
211 ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl] |
211 qpair_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl] |
212 addSDs [QInl_inject,QInr_inject]; |
212 addSDs [QInl_inject,QInr_inject]; |
213 |
213 |
214 goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A"; |
214 goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A"; |
215 by (fast_tac qsum_cs 1); |
215 by (fast_tac qsum_cs 1); |
216 val QInlD = result(); |
216 val QInlD = result(); |
217 |
217 |