[isabelle-dev] An ARBITRARY question

2008-10-03 Thread Lawrence Paulson
What is the difference between willundefined and arbitrary? Larry On 2 Oct 2008, at 18:44, Tobias Nipkow wrote: 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

[isabelle-dev] An ARBITRARY question

2008-10-03 Thread Lawrence Paulson
Apologies for that garbled message. I meant, What is the difference between undefined and arbitrary? Larry On 2 Oct 2008, at 18:44, Tobias Nipkow wrote: undefined and default are used in a specific way. If you do not want that functionality (and accidental equalities), arbitrary

[isabelle-dev] An ARBITRARY question

2008-10-03 Thread Tjark Weber
On Fri, 2008-10-03 at 14:14 +0200, Florian Haftmann wrote: I also think that two would be better than three; technically undefined is the same as arbitrary Then what is the point of undefined_fun: undefined x = undefined in HOL.thy? Best, Tjark

[isabelle-dev] An ARBITRARY question

2008-10-03 Thread Florian Haftmann
Then what is the point of undefined_fun: undefined x = undefined in HOL.thy? This is essentially pointless and is so soon to be dropped that I didn't take the effort to even point out to it in my emails, taking the risk that somebody would have a look a the source ;-) Florian

[isabelle-dev] An ARBITRARY question

2008-10-02 Thread 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

[isabelle-dev] An ARBITRARY question

2008-10-02 Thread Tobias Nipkow
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