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 ;-).



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.