Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Hyperlinked ZF?

view this post on Zulip Email Gateway (Aug 18 2022 at 16:41):

From: Victor Porton <porton@narod.ru>
There are <http://isarmathlib.org/> which presents hyperlinked theories based
on Isabelle/ZF but in that site is missing presentation of ZF core.

Are there anywhere a hyperlinked presentation of Isabelle/ZF?

Or maybe I can build it myself, can't I?

\--
Victor Porton - http://portonvictor.org

view this post on Zulip Email Gateway (Aug 18 2022 at 16:41):

From: Alexander Krauss <krauss@in.tum.de>
Victor Porton wrote:
Isarmathlib and the software that generates the HTML isn't maintained by
the Isabelle team. Maybe the author can help you there.

There is also a HTML version generated from the main ZF theorie, but it
is much less pretty: http://isabelle.in.tum.de/dist/library/ZF/index.html

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 16:42):

From: Slawomir Kolodynski <skokodyn@yahoo.com>
The tool that generates HTML from IsarMathLib theories can parse only a limited subset/dialect of Isar that IsarMathLib uses. It can not parse standard Isabelle/ZF theories included in the distribution.

slawekk

Last updated: Apr 20 2024 at 01:05 UTC