Re: [isabelle] Method combinator ; restricts to first subgoal



> On 6 Jun 2015, at 3:52 am, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>
> An aside on this thread: the ';' combinator provides a nice way for
> transferring class instances to parametric types, e.g. in
> ~~/src/HOL/NSA/StarDef.thy
>
>> instance star :: (order) order
>> apply (intro_classes)
>> apply (transfer, rule less_le_not_le)
>> apply (transfer, rule order_refl)
>> apply (transfer, erule (1) order_trans)
>> apply (transfer, erule (1) order_antisym)
>> done
>
> can now be simply written as
>
>> instance star :: (order) order
>>  by (intro_classes; transfer) (fact less_le_not_le order_refl order_trans order_antisym)+

You could also write it as

> (intro_classes; transfer; fact less_le_not_le order_refl order_trans order_antisym)

Which is not that useful here, but generally more appropriate in an apply-script (where "+" has a tendency to over-step).

Regards,
Dan


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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