Re: [isabelle] The Incredible Proof Machine



Nice work.

Just one experience when I played around with it, which puzzled me, and
might severely puzzle your students: I tried A&B&C ==> A&C, my attempt
is attached.

As I did not know whether & binds to left or right, I ended up attaching
the line to the wrong exit. But then, I got an error on the line from
the start, which was fine previously. I.e., when I attach something to a
block, I may get an error at a seemingly unrelated point.

Moreover, if I have something like
  A&B&C ---> (dest-AND) 

I would like to "see" which propositions are available at the outputs.

-- Peter

Attachment: incredible-proof.svg
Description: image/svg



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