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. Larry > On 8 Jul 2017, at 22:16, Peter Lammich <lamm...@in.tum.de> wrote: > > We already have proof goal_cases. Is that what you mean?
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
