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?


	Makarius


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