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"
https://bitbucket.org/isabelle_project/isabelle-release/commits/ae53f4d901a3
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).


	Makarius





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