Email Gateway (Aug 19 2022 at 12:03): Email Gateway (Aug 19 2022 at 12:03):From: Alfio Martini <alfio.martini@acm.org>
Hi,
I am not sure if the we can assume that documentation is updated
already, but
in section 6.3.1 (Relations) of the Isabelle/HOL Tutorial, relation
composition
is now labelled as 'relcomp_unfold" and not as 'rel_comp_def'.
There may be some more inconsistencies.
Moreover, 'thm mem_Collect_eq' does not pretty print in the Output
pane exactly like in the tutorial documentation.
Cheers
Email Gateway (Aug 19 2022 at 12:03):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks for the report, and I have fixed 'rel_comp_def', but not the other one,
which I leave to its author. Unfortunately that part of the book was not written
with sustainability in mind, i.e. no antiquotations, and hence it is virtually
impossible to keep it up-to-date. But since the proofs in there do not reflect
the state of the art anymore either, let's just say that anything in that
tutorial needs to be taken with a grain of salt.
Tobias
Last updated: May 01 2024 at 20:18 UTC