"undefined" and "default" are used in a specific way. If you do not want that functionality (and accidental equalities), "arbitrary" is a good alternative.
Tobias Florian Haftmann schrieb: > 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 > > > > ------------------------------------------------------------------------ > > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
