[isabelle] Min shadowing
When using HOL-Analysis, Min refers by default to linorder_class.Min.
However, when I import "HOL-Decision_Procs.Approximation", then Min
refers now to floatarith.Min, and I have to replace all my uses of Min
by linorder_class.Min to get everything straight.
What would be the best way to hide floatarith.Min so that Min still
refers to linorder_class.Min? (What I would like to do is import
Approximation in its own namespace, for instance.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and