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
next
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 :-)
>
> Cheers,
>
> Steven
>




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