Re: [isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
quick (unrelated) question ;)
How is your "open inductive" related to the AFP entry "Open Induction"?
On 02/23/2015 04:38 PM, Joachim Breitner wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and