Re: [isabelle] Collections: problems with sets of sets



Hi all,

> The problem goes away when I remove the [code nbe] declaration that
> comes after the instance proof of equal in Dlist.thy
> (http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/HOL/Library/Dlist.thy#l128).
> I don't know about the precise semantics of [code nbe] wrt. normal code
> equations, but it seems to override the previous code equation.

all [code …] declarations simply override any default equation.

Btw. the explicit declaration is currently tested for addition.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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.