Re: [isabelle] IsarMathLib

Dear Omar,

> 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
> sledgehammer?

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