Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Minor Error in Isabelle Referece Manual

view this post on Zulip Email Gateway (Jan 03 2024 at 12:32):

From: Gunnar Teege <gunnar.teege@unibw.de>
Hello all and a happy new year,

there seems to be a minor error in the ref manual concerning the syntax
ob obtains and consider (and also obtain?). In the syntax diagrams in
6.2.4 and in the grammar in A.1.1 and Fig. 2.2 the "vars where" part is
described as mandatory which does not match with the examples and the
isabelle behavior where it can be omitted.

Best regards

Gunnar Teege

smime.p7s

view this post on Zulip Email Gateway (Jan 12 2024 at 16:17):

From: Makarius <makarius@sketis.net>
Thanks. I have now refined the documentation here:
https://isabelle-dev.sketis.net/rISABELLE590a01e3efb4

Note that only the railroad diagrams attempt to describe the true
implementation. Everything else is just illustrate, with optional parts
written like they were mandatory.

Makarius

Last updated: Jan 04 2025 at 20:18 UTC