Stream: Beginner Questions

Topic: Backwards compatibility

Ant S. (Feb 12 2026 at 22:08):

I found these slides for Isabelle from c. 2007
http://typessummerschool07.cs.unibo.it/#introduction
http://typessummerschool07.cs.unibo.it/courses/nipkow.tgz

A lot of the syntax such as text {* ... *} or import PreList raises an exception. Is this a compatibility issue for something that was renamed in future versions of Isabelle?

Ant S. (Feb 12 2026 at 22:50):

apparently text comments are now text \open< ... \close>

Ant S. (Feb 12 2026 at 22:50):

when/where was this change made

Balazs Toth (Feb 12 2026 at 23:01):

It was made incompatible in the 2018 version

https://isabelle.in.tum.de/repos/isabelle/file/tip/NEWS
(line 4108)

Manuel Eberl (Feb 15 2026 at 08:52):

Generally speaking, Isabelle changes a lot. Everything in the Archive of Formal Proofs is kept up to date, but everything outside of it tends to succumb to bit rot after a free years. Twenty year old stuff is probably unusable. But if you need help with anything specific, do feel free to ask!

Last updated: Mar 04 2026 at 20:34 UTC