Re: [isabelle] The Incredible Proof Machine

Dear Peter,

Am Donnerstag, den 24.09.2015, 17:54 +0200 schrieb Peter Lammich:
> 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.

Right. One of my ideas is to keep track of the order in which
connections have been added (or been changed), and apply unification in
that order. In fact, I think I forgot that I planned to do this, so I
better create an issue for it:

> Moreover, if I have something like
>   A&B&C ---> (dest-AND) 
> I would like to "see" which propositions are available at the
> outputs.

You can always âpull outâ a connection (without connecting it to
something else) and see whatâs on it. But it would be more convenient
to see something right away; this is also planned:


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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