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



Hi list,

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.

However, the solves is quite tedious to write: When developing the
proof, you can only add it after your method works. And if something
breaks, you have to remove the solve to inspect the failure.
Is it possible to have some nice short suffix syntax for solves,
something like "apply auto!", similar to "apply auto []" ?

Can such a syntax be declared in without changing Isabelle, or would it
require a modification of the Isabelle sources?

--
  Peter






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