[isabelle] Sequents.thy



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



 




-- 
Paqui Lucio
Facultad de Informática
Universidad del País Vasco
SPAIN







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