[isabelle-dev] type class ordered_semiring_1

[Lawrence Paulson]

This type class is defined in a number of AFP entries. Unfortunately, the definitions used are not the same and it's not clear whether they are equivalent either. We ought to fill this gap, though I am not sure of the best way to do it. In LLL_Basis_Reduction/Missing_Lemmas it is used to generalise a number of simple results currently proved for a smaller type class, ordered_idom.

Larry