[isabelle-dev] unit :: complete_boolean_algebra – 697e0fad9337
andreas.lochbihler at inf.ethz.ch
Wed Jun 11 09:22:22 CEST 2014
the simproc unit_eq in
rewrites anything of type unit to (), so there's no need to declare the definitions
introduced in 697e0fad9337 as [simp]. One could declare sup_unit_def, inf_unit_def,
Sup_unit_def, and Inf_unit_def as [abs_def, simp] such that they get unfolded even if they
are applied only partially, but I don't know whether that is a good thing to have.
(Admittedly, the definition of uminus has this [simp] declaration, so it's a bit
unconsistent at the moment).
On 10/06/14 23:02, Florian Haftmann wrote:
> Hi Andreas,
> I'm wondering whether there is a deliberate reason to declare top, bot
> etc. on unit not as simp by default. Since there is only one element of
> unit, proof goals after simp should be trivial…
More information about the isabelle-dev