Re: [isabelle] Proof automation for Types_To_Sets

On 18/11/16 15:34, Andreas Lochbihler wrote:
> Dear list, dear Ondrej and Andrei,
> I've tried out the new Types_To_Set and I find it very convenient to
> clean my proofs from unnecessary invariants. However, I am a bit
> unsatisfied with the level of proof automation. In the ITP2016 paper, it
> says that the transfer "tool is able to perform the relativization
> completely automatically".

At ITP / Nancy I have actually encouraged Ondrej and Andrei to put this
experiment into shape for the Isabelle2016-1.

So far the release branch has nothing else than the "initial commit"
without any official description in NEWS whatsoever.

This is OK, but it should be made clear that it is just a
proof-of-concept that accompanies the very first conference paper
introducing the ideas behind it (I have myself looked at the paper only
for 2h: from 3am to 5am one summer night at Nancy).


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