[isabelle] Basic question about apply-style reasoning



Hi all,

I have a goal of the form:
 I a b ==> I a' b'

how to transform this goal into
   a=a' &&& b=b'
which can (in my case) be easily solved by auto.
Optimal would be a proof like this:
   by (auto {intro,elim,dest,simp}: some_rule)

I tried to find an adequate rule via find_thms, but had no success.

Best,
 Peter





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