See now http://isabelle.in.tum.de/repos/isabelle/rev/a1a4a5e2933a
Cheers
Florian
Am 28.10.2017 um 16:14 schrieb Florian Haftmann:
> Hi Akihisa,
>
> thanks for pointing that out.
>
> I will take care of this.
>
> All the best,
> Florian
>
> Am 20.10.2017 um 17:37 schrieb Yamada,
Hi Akihisa,
thanks for pointing that out.
I will take care of this.
All the best,
Florian
Am 20.10.2017 um 17:37 schrieb Yamada, Akihisa:
> Dear Isabelle/HOL developers,
>
> I propose to make linordered_semiring_1 a subclass of zero_less_one.
>
> class linordered_semiring_1 =
>
Dear Isabelle/HOL developers,
I propose to make linordered_semiring_1 a subclass of zero_less_one.
class linordered_semiring_1 =
linordered_semiring + semiring_1 + zero_less_one
(Of course, zero_less_one should be defined earlier.)
Currently, it does not assume 0 < 1, but this generality
