Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle 2025 import issues

view this post on Zulip Email Gateway (Nov 17 2025 at 06:20):

From: Changyang Zeng <cl-isabelle-users@lists.cam.ac.uk>
Hi users of Isabelle,

I am new to Isabelle and confused about importing the HOL-Library.Word
issue.

I have a ROOT file as below:

session "Test" = "HOL-Library" +
  theories
    "Test"

The Test.thy is defined as below:
···
theory Test
imports Main
"HOL-Library.Word"
begin

term "popcount"
value "(3 :: 32 word) + 5" (* Simple test *)
value "shiftl (3 :: 8 word) 1"
value "0b1101 >> 2"
···

The result of value "shiftl (3 :: 8 word) 1" in the output panel is:
"shiftl 3 1"
:: "'b"

I opened these two files in the Isabelle Jedit IDE.
The result of value "0b1101 >> 2" in the output panel is Inner syntax error
Failed to parse term.

My guess is that I did not import HOL-Library.Word successfully, therefore
Isabelle does not recognize the operators from HOL-Library.Word, even
though I did see this theory in the Theories panel. So I am wondering how
to import it correctly. Also I would like to confirm if popcount is a
built-in function in Isabelle, as suggested by the generative AI.

Thank you so much for taking time on my doubts, I look forward to your help!

Best,
Changyang

view this post on Zulip Email Gateway (Nov 17 2025 at 09:57):

From: Makarius <makarius@sketis.net>
On 17/11/2025 07:19, Changyang Zeng (via cl-isabelle-users Mailing List) wrote:

So I am wondering how to import it
correctly. Also I would like to confirm if popcount is a built-in function in
Isabelle, as suggested by the generative AI.

At the end of the mail we have the actual problem.

Please think for yourself and apply common-sense.

Makarius

view this post on Zulip Email Gateway (Nov 18 2025 at 04:34):

From: Changyang Zeng <cl-isabelle-users@lists.cam.ac.uk>
Thanks Makarius I think I figured out these issues.

On Mon, Nov 17, 2025 at 1:57 AM Makarius <makarius@sketis.net> wrote:

On 17/11/2025 07:19, Changyang Zeng (via cl-isabelle-users Mailing List)
wrote:

So I am wondering how to import it
correctly. Also I would like to confirm if popcount is a built-in
function in
Isabelle, as suggested by the generative AI.

At the end of the mail we have the actual problem.

Please think for yourself and apply common-sense.

Makarius

Last updated: Dec 02 2025 at 16:32 UTC