Hi Brian
Every time I use the overloaded constants top and bot (defined in
Orderings.thy), Isabelle prints them out as top_class.top and
bot_class.bot, instead of just top and bot. I find this
annoying, so I tried to find out the reason for this.
class top = preorder +
fixes top :: 'a
On Mon, May 3, 2010 at 4:55 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
class top = preorder +
fixes top :: 'a
assumes top_greatest [simp]: x \le top
class bot = preorder +
fixes bot :: 'a
assumes bot_least [simp]: bot \le x
The fact that both class
