Re: [isabelle] Proof automation for Types_To_Sets
- To: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] Proof automation for Types_To_Sets
- From: Makarius <makarius at sketis.net>
- Date: Sat, 3 Dec 2016 16:07:38 +0100
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1
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