Re: [isabelle] IsarMathLib
> Can I use "IsarMathLib" library in Isabelle?
Probably -- but I'll let others who know IsarMathLib and Isabelle/ZF better answer this.
> and where I can put this
> library file to work correctly with Isabelle commands like nitpick and
Unfortunately, Nitpick and Sledgehammer are limited to Isabelle/HOL. However, Nitpick's successor, Nunchaku, is currently being developed, and we aim at targeting set theory as well (Isabelle/TLA and Isabelle/ZF), so that it could be used in conjunction with IsarMathLib. As for Sledgehammer, we also want to generalize in the same direction, but have currently no financing or student working on that.
This archive was generated by a fusion of
Pipermail (Mailman edition) and