Re: [isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop



Dear Joachim,

quick (unrelated) question ;)

How is your "open inductive" related to the AFP entry "Open Induction"?

cheers

chris

On 02/23/2015 04:38 PM, Joachim Breitner wrote:
Dear list,

what is usually the cause for the error message

         *** exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop

To reproduce with Isabelle-2014, run
$ git clone https://github.com/gattschardo/open-inductive
$ cd open-inductive
add "Open_Arith_Eval" to "theories" in ROOT
$ isabelle build -D .


It does not (seem to) occur in Isabelle/jEdit.

Thanks,
Joachim






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