On Fri, 26 Aug 2011, Brian Huffman wrote:
On Fri, Aug 26, 2011 at 2:02 PM, Andreas Schropp <schr...@in.tum.de> wrote:
So you suggest using e.g.
if EX x. x : A then A
else {0}
instead of A as the semantic interpretation?
Interesting!
Yes, this is exactly the kind of thing I meant. You could use any
nonempty set you want in place of {0}, of course.
How about {undefined}, or similar?
You surely know this HOL joke in some form or the other:
"if default = undefined then SOME x. True else SOME x. False"
(Attributed to F. Haftmann?)
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
