Re: [isabelle] Short syntax for "solves <method>"



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.


	Makarius




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