[isabelle-dev] NEWS

[Amine Chaieb]

Very nice job!

Amine.

PS: In Reflected Ferrack you start combutation with True, i.e. @{code 
T}, if the input is @{term False}. Fortunately this does not happen 
often.... Even with @{code} we still need to be careful...


Florian Haftmann wrote:
> New ML antiquotation 'code': takes constant as argument, generates
> corresponding code in background and inserts name of the corresponding
> resulting ML value/function/datatype constructor binding in place.  All
> occurences of 'code' with a single ML block are generated simultaneously.
> Provides a generic and safe interface for instrumentalizing code
> generation.  See HOL/ex/Code_Antiq for a toy example, or
> HOL/Complex/ex/ReflectedFerrack  for a more ambitious application.  In
> future you ought refrain from  ad-hoc compiling generated SML code on
> the ML toplevel.
> Note that (for technical reasons) 'code' cannot refer to constants for
> which user-defined serializations are set.  Refer to the corresponding
> ML counterpart directly in that cases.
> 
> 	Florian
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev