[isabelle] [Fwd: Re: Qualified name for Set.insert]



--- Begin Message ---
Hi Peter,

>   *** No such constant: "Set.insert"
> *** At command "lemma".

"insert" belongs to a ancient set of constants that habe a non-qualified
name.

> My current workaround is to define an abbreviation "set_insert ==
> insert" before I re-define the constant or rename my own constant to,
> e.g. "insrt".

This is indeed the best workaround I am aware of.

In the next Isabelle release, insert will be qualified :-).

Hope this helps
	Florian

-- 

Home:
http://wwwbroy.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


--- End Message ---


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