Re: [isabelle] undefined & None



>> * Constants "undefined" and "default" replace "arbitrary".  Usually
>> "undefined" is the right choice to replace "arbitrary", though
>> logically there is no difference.  INCOMPATIBILITY.

Indeed the maior issue was the introduction of a separate »default«
beside »arbitrary«, where »default« is a type class parameter.  It seems
that only proof extraction does really use »default«, so this might
count as argument ot move »default« to Extraction.thy.

Concerning the naming of the constant now named »undefined«, my opinion
is just unspecified ;-).

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.