Re: [isabelle] Basic question about apply-style reasoning

Probably, you mean arg_cong and arg_cong2 ??? A theorem named app_cong does not exist.

   apply (subst arg_cong2[where f=I]) by auto
does the job, but introduces some odd-looking schematic variables in between.


Lars Noschinski schrieb:
On 03.05.2011 15:13, Peter Lammich wrote:
I have a goal of the form:
I a b ==> I a' b'

how to transform this goal into
a=a' &&& b=b'

Have a look at the rules app_cong and app_cong2. You may need to instantiate them first.

  -- Lars

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