[isabelle-dev] An ARBITRARY question

[Florian Haftmann]

Some years ago two further constants were introduces into HOL.thy:
"undefined" and "default".  The idea then was to divide the role of
classical "arbitrary" on two shoulders:  "undefined" should be
unspecified an could be used to fake partiality, whereas "default" would
be overloaded and could be instantiated on arbitrary types, which is
useful e.g. for proof extraction.  Meanwhile the code dealing with
unspecified case clauses and missing primrec equations etc. has already
switched from "arbitrary" to "undefined".

I would suggest to walk through and drop any remaining occurence of
"arbitrary" by "undefined".

But perhaps "arbitrary" is too deep-rooted in HOL tradition to just get
rid of it.  Any further arguments against?

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20081002/0bf82e20/attachment.sig>