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



On 03.05.2011 15:58, Peter Lammich wrote:
Probably, you mean arg_cong and arg_cong2 ??? A theorem named app_cong
does not exist.

Yes, sorry.

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

In your case, this rule is more suitable as an introduction rule, i.e.

   by (rule arg_cong2[where f=I]) auto

  -- Lars





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