[isabelle] Isabelle2014-RC0: add_assoc hidden, causes error, but proof passes



Hi,

There's "Groups.semigroup_add.add_assoc", followed in Groups.thy by "hide_fact add_assoc". The "hide_fact" is new in Groups.thy and causes an error in a proof.

The proof passes even through there's an error 'Undefined fact: "add_assoc"'. I attach a screen shot showing the error.

Trying to fix that problem, I ran Sledgehammer and have a more serious problem, which is that Cygwin temp files can't be deleted, which causes the prover process to terminate. I'll put that that in another email.

Regards,
GB


Attachment: Hidden_add_assoc_error.png
Description: PNG image



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