Re: [isabelle] Problems with Sequents in Isabelle



On Fri, 9 Feb 2007, Peter Chapman wrote:

> Another problem, though.  Now I'm trying to implement the sequent calculus
> G3ip.  The whole file builds/loads until the last line, which is
> 
> ML {* use_legacy_bindings (the_context ()) *}
> 
> which spits back the error
> 
> *** Error:
> *** Can't unify bool with Thm.thm (Different type constructors) found near
> ***     val false = thm("false")
> ***
> ***
> ***  Failure
> *** At command "ML" .

Here SML complains about an attempt to use an existing constructor (false) 
in a thm value binding.  This kind of incident explains why the above 
function is called use_legacy_bindings -- you probably won't need these 
bindings anyway.


> I wrote a file called G3ip.ML similar to LK0.ML

This is another legacy feature.  There is no need to use ML files, just 
produce plain Isar sources.  E.g. see the version of Sequents in recent 
Isabelle development snapshots, which no longer feature these strange ML 
things.


	Makarius





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