Re: [isabelle] Problems with Sequents in Isabelle



Thanks.

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


I don't know which file it is looking at with the line `` val false = thm("false") ``. I wrote a file called G3ip.ML similar to LK0.ML, but still got the error (I don't know if that is where the error comes from in the first place). I can't find anything in the documentation, or a few hours worth of internet searching, to tell me how to fix this error, or even what is causing it.

The top line for my file, if that is relevant, is

theory G3ip
imports Sequents

begin
.
.
.

Any help would be greatly appreciated.

Cheers

Peter Chapman





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