Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Solved it: Setsum Subgoal with play on the ind...

Email Gateway (Aug 17 2022 at 14:15):

From: Primrose.Mbanefo@Infineon.com
Hi,

I used "setsum_reindex_cong[of "(%x. Suc x)"])"
and that worked (with some other stuff but it was basically what I was
missing).

Thanks to anyone who spent anytime on this.

Regards,
Primrose

Last updated: May 03 2024 at 12:27 UTC