[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.)

Sebastien





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.