[isabelle-dev] adhoc overloading

[Florian Haftmann]

>> There is no point to do
>> such low-level optimizations in the syntax layer.  It is for hardcore
>> kernel operations only
> 
> So should I manually check the result for equality, or does the
> framework do this for me?

See
http://isabelle.in.tum.de/repos/isabelle/file/41d7946e2595/src/Pure/Syntax/syntax_phases.ML#l854

There are two variants of interfaces adding functions to check phases:
one with explicit hinting by the check function via None/Some, the other
one with check by the framework.

	Florian

-- 

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

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