Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sequents.thy

view this post on Zulip Email Gateway (Aug 18 2022 at 11:27):

From: Paqui Lucio <paqui.lucio@ehu.es>
Hi,
Trying to load in Isabelle (version 2005) the archive Sequents.thy,
which I have downloaded from the Isabelle page, I found two problems
that I cannot solve. First, in the line 11:

declare [[unify_trace_bound = 20, unify_search_bound = 40]]

*** Outer syntax error: name reference expected,
*** but keyword "[" was found

and second (when I commented the line 11) just before the end:

use "prover.ML"

*** Outer syntax error: name reference expected,
*** but keyword "[" was found

Could somebody tell me why?
Thanks in advance,
Paqui

Paqui Lucio
Basque Country University

view this post on Zulip Email Gateway (Aug 18 2022 at 11:28):

From: Alexander Krauss <krauss@in.tum.de>
The files you downloaded are for Isabelle 2007.

Alex

Last updated: Nov 21 2024 at 12:39 UTC