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
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