Re: [isabelle] Isabelle 2013-1 RC2 (Documentation)
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.
Am 12/10/2013 20:12, schrieb Alfio Martini:
> 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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and