Re: [isabelle] Getting cong to work with carriers



You may have luck with 

   apply (auto cong: rule_cong simp add: simp_rule subsetD [OF 1])

Auto doesn’t use “elim!” inside the simplifier, but outside it, so it cannot help.

The point of my suggestion is to instantiate the variables in subsetD.

Larry

On 9 Aug 2014, at 10:20, Holden Lee <hl422 at cam.ac.uk> wrote:

>    apply *(auto cong: rule_cong simp add: simp_rule elim!: subsetD)*





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