Theory Rat (formerly Rational) has a function called "normalize". This is
a rather generic name for main HOL -- today I've seen a user theory where
it has caused a clash. (It was easy to fix by using an explicit binding
in the 'definition' command in question, but it is confusing nonetheless.)
Is there a better name for Rat.normalize? Alternatively, one could just
use hide_const (open) in theory Rat as is now done for many other things
in main HOL.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
