Re: [isabelle] Short syntax for "solves <method>"
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] Short syntax for "solves <method>"
- From: Makarius <makarius at sketis.net>
- Date: Sat, 9 Jan 2016 20:45:54 +0100 (CET)
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <1437045966.32412.6.camel@lapnipkow10>
- References: <1437045966.32412.6.camel@lapnipkow10>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Thu, 16 Jul 2015, Peter Lammich wrote:
one of the Eisbach features that I use most is the solves-method.
In an apply-style script, I write "solves <auto>" and the like for
documentation purposes: This method is intended to solve the goal. This
makes apply-scripts much more maintainable.
Isabelle2016-RC0 allows a more systematic form:
subgoal by auto
Note that such higher structures don't work with schematic goals.
This archive was generated by a fusion of
Pipermail (Mailman edition) and