Re: [isabelle] Sequents.thy

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

The files you downloaded are for Isabelle 2007.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.