Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bad theory import "HOL-Library.Type_Length" in...


view this post on Zulip Email Gateway (Aug 23 2022 at 08:52):

From: Xingyuan Zhang <xingyuanzhang@126.com>
Hi,
When I opened ~~/src/HOL/Word/Word.thy in Isabelle-2019/vs code, the following errors appeared in Isabelle/Output panel:

Bad theory import "HOL-Library.Type_Length"
Bad theory import "HOL-Library.Boolean_Algebra"

The problem happened only in Isabelle/vs code, not in Isabelle/jEdit, I would guess it is a bug in vs code.
Could any body give any help?

Xingyuan

view this post on Zulip Email Gateway (Aug 23 2022 at 08:53):

From: Makarius <makarius@sketis.net>
Isabelle/VSCode does not work in Isabelle2019: the VSCode project has been
moving too fast away from Isabelle.

We are already approaching the final publication of Isabelle2020 (scheduled
for 15-Apr-2020). You can already use
https://isabelle.in.tum.de/website-Isabelle2020-RC5 right now.

Makarius


Last updated: Mar 28 2024 at 20:16 UTC