Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] 2025-RC1: issue with `inclduing` command

Email Gateway (Feb 04 2025 at 10:05):

From: "\"Putti, Edoardo (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear list,

The including command now accepts one bundle name only. This is a regression and the documentation refers to including as the counterpart to using which accepts multiple identiefiers.

The following example is enough to ttrigger the problem and the error message reports "Outer syntax error⌂: command expected ,but identifier b was found".

theory Scratch
imports Main
begin

bundle a
begin
end

bundle b
begin
end

lemma "True"
including a b
oops
end

Email Gateway (Feb 04 2025 at 10:15):

From: Makarius <makarius@sketis.net>
On 04/02/2025 11:04, "Putti, Edoardo (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:

The |including| command now accepts one bundle name only. This is a regression
and the documentation refers to |including| as the counterpart to |using|
 which accepts multiple identiefiers.

This is merely a change of syntax, see "isar-ref" page 97 for "bundles" or
this NEWS entry:

• Command "unbundle b" and its variants like "context includes b" allow
  an optional name prefix with the reserved word "no": "unbundle no b"
  etc. This reverses both the order and polarity of bundled declarations
  like 'notation' vs. 'no_notation', and thus avoids redundant bundle
  definitions like "foobar_syntax" vs. "no_foobar_syntax", because "no
  foobar_syntax" may be used instead. Consequently, the syntax for
  multiple bundle names has been changed slightly, demanding an explicit
  'and' keyword. Minor INCOMPATIBILITY.

  Makarius

Last updated: Mar 09 2025 at 12:28 UTC