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

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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