Re: [isabelle] Sublocale, subclass and execution.



Hi Clemens,

> I like your idea of using more descriptive keywords here.  Following
your suggestion, 'where' could be called 'unfolding' and replaced by
'folding' if we decide to turn the rewrite equations around.  However,
the ing form tends to be used by the proof language for transformations
of the proof state, and 'unfolding' would even make the grammar
ambiguous.  It will probably make more sense to settle for 'defines',
'unfolds' and 'folds'.

I agree in principle, but I am still uncertain what the preferred
orientation for mixin equations should be, except that there should only
be one orientation.

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.