On 24.04.2013 16:18, Brian Huffman wrote:
On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel tray...@in.tum.de wrote:
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) = λ(c, d). e) y
Usually prod_case
I discovered a problem with the pretty-printing of some terms (I am
using revision 4392eb046a97).
term (λ(a, b) (c, d). e) x y
case_guard True x
(case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d). e
case_nil)
y
:: 'e
I assume this is a result of the recent changes
Am Mittwoch, den 24.04.2013, 11:45 +0200 schrieb Tjark Weber:
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
Hi all,
since Containers are in the AFP mira results in global crashes of the
build tool
(http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694).
By global I mean that no session is built at all due to an outdated (wrt
Isabelle repository, e.g. 916271d52466)
Am Donnerstag, den 25.04.2013, 10:56 +0200 schrieb Johannes Hölzl:
I also renamed the type class linear_continuum_topology to
connected_linorder_topology as they are not compact spaces. If somebody
knows a better name for these spaces I'm also happy to rename them.
Okay, forget this.
