Re: [isabelle] "and similarly..."
If you were writing tactics (i.e. using "apply-style" proofs), you could
use function abstraction. For example:
fun foo m = ...
then in the proof:
apply foo HeadMap
apply foo TailMap
But this is not very robust, and I don't know if there's anything
equivalent in "proper" (structured) Isar.
On Tue, Jan 31, 2012 at 4:07 PM, Steven Obua <steven.obua at googlemail.com>wrote:
> On 31.01.2012, at 15:57, John Wickerson wrote:
> > Hello,
> > Is there a feature in Isabelle that corresponds to writing "and
> similarly" in an informal pen-and-paper proof?
> This question made my day :-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and