Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] wrong documentation in Isabelle/Isar Reference...

view this post on Zulip 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

smime.p7s

view this post on Zulip 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: Jan 04 2025 at 20:18 UTC