No, that’s precisely what I’d like to avoid. I prefer texts that you can 
actually read. It would be great to have something automatically generated, 
even if it needed manual tweaking (e.g. to rename variables).

And I’ve gone to some effort purging instances of “guess” from existing proofs.


> On 8 Jul 2017, at 22:16, Peter Lammich <> wrote:
> We already have proof goal_cases. Is that what you mean?

isabelle-dev mailing list

Reply via email to