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

An aside on this thread: the ';' combinator provides a nice way for
transferring class instances to parametric types, e.g. in

> 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)+



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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