See now 7faa9bf9860b for a related issue.
We had a personal conversation that it is very likely that the remaning
issues will disappear after the next big envisaged reform of the
analysis material.
Cheers,
Florian
Am 07.08.2016 um 10:47 schrieb Florian Haftmann:
> Hi Johannes,
>
> that
Hi Johannes,
that change had probably more pervasive effects than intended. E.g. the
definition
definition (in comm_monoid) operative …
and its basic lemmas now produce the following soup of theorems
thm inf_top.operative_def sup_bot.operative_def add.operative_def
mult.operative_def
