Johannes,
On Mon, 2013-04-22 at 16:39 +0200, Johannes Hölzl wrote:
* Introduce type class conditional_complete_lattice: Like a complete
lattice but does not assume the existence of the top and bottom elements.
The name conditional complete lattice suggests a special kind of
complete lattice.
Hi Brian
thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense
that internal constants (like case_guard) are not visible anymore.
However, your example is still not printed as expected (assuming that
the output should be equal to the input in this case):
(case x of (a, b)
On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel tray...@in.tum.de wrote:
Hi Brian
thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense that
internal constants (like case_guard) are not visible anymore.
Thanks for taking care of this so quickly!
However, your example is
But for the moment I will leave this aside anyway.
Still one thing to add:
http://isabelle.in.tum.de/repos/isabelle/rev/cb154917a496
avoids the odd reinit entirely, the critical lines being
fun add_dependency locale dep_morph mixin export =
(Local_Theory.raw_theory ooo
Hi,
Am Mittwoch, den 24.04.2013, 19:16 +0200 schrieb Florian Haftmann:
This is a great triumph of the »local everything« approach.
I’m not sure that I understand all that is going on, but I have the
feeling that the theory that I’m working on will greatly benefit from
your development, and I’m
