Email Gateway (Aug 30 2023 at 09:02): Email Gateway (Aug 30 2023 at 09:02):From: Gunnar Teege <gunnar.teege@unibw.de>
Hello,
in section 11.7.3 of isar-ref.pdf the documentation for the record
update operation is wrong. It states that the first argument of an
update operation ci_update for a field ci is the new value to be set.
Instead, the implementation takes as first argument an update function
from the old value of ci to its new value.
I assume that this is a left-over from an earlier record implementation.
All necessary changes should be on page 271.
Perhaps it is still possible to correct this for the 2023 release.
Best regards
Gunnar Teege
Email Gateway (Aug 30 2023 at 15:12):From: Makarius <makarius@sketis.net>
Thanks.
I have updated it for the release as follows:
https://isabelle.sketis.net/repos/isabelle-release/rev/6aa964f52395
changeset: 78580:6aa964f52395
tag: tip
user: wenzelm
date: Wed Aug 30 17:02:40 2023 +0200
files: src/Doc/Isar_Ref/HOL_Specific.thy
description:
more accurate documentation of record field update, following changes in
Isabelle2007 and Isabelle2008;
Makarius
Last updated: Apr 28 2024 at 20:16 UTC