[isabelle-dev] NEWS: Rat in Isabelle/ML

[Makarius]

On 01/06/16 21:58, Florian Haftmann wrote:
> 
> One could regard the dedicated literal syntax for rationals a little bit
> oversophisticated;  maybe an infix // for Rat.make would serve better.
> Or we could A matter of personal taste, though.

There is a delicate point here: our antiquotation infrastructure
distinguishes inlined text from compile-time values. @a/b is the latter,
so it is always guaranteed to be pre-evaluated, independently of other
code inline options of Poly/ML.

This is also the reason why I have removed Rat.zero, Rat.one, Rat.two
and used @0, @1, @2 everywhere.


	Makarius



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160601/ea05ef8c/attachment.sig>