Re: [isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
On Tue, 24 Feb 2015, Joachim Breitner wrote:
I have more to say about the sources, but that has to wait.
A review of that code would be highly appreciated â you can probably
tell that it was not written with a great lot of experience with and
comprehensive knowledge of the Isabelle internals.
It is fine as a first project to implement an Isabelle "package". I can
offer a standard pencil-review on the sources, with scanned results sent
back (privately). This could help to make one more round of refinement,
and then proceed to more deeper points.
I suppose this work is meant for AFP?
This archive was generated by a fusion of
Pipermail (Mailman edition) and