[isabelle] Meta_impE and other tactics



Hi

I have the following premisses and goal (the details are unimportant, it is the structure which is important):

[|  [| A ; B |] ==> C ; D ; E ; A ==> D ; B ==> E |] ==> C

I think this should be provable, I rewrite using the A ==> D and B ==> E inside the inner [| |] to get

[| [| D ; E |] ==> C ; D ; E |] ==> C

to

C

Is this logically sound? How can I rewrite the A and B within the inner brackets?

Thanks in advance

Peter







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