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.
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