Fri, 20 May 2011 16:22:24 +0200simp rules for empty intervals on dense linear order
hoelzl [Fri, 20 May 2011 16:22:24 +0200] rev 43762
simp rules for empty intervals on dense linear order

Fri, 20 May 2011 14:12:59 +0200merged
wenzelm [Fri, 20 May 2011 14:12:59 +0200] rev 43761
merged

Fri, 20 May 2011 14:03:42 +0200removed some obsolete text;
wenzelm [Fri, 20 May 2011 14:03:42 +0200] rev 43760
removed some obsolete text;

Wed, 18 May 2011 23:39:22 +0200basic support for overpainting of text, imitating jEdit internals;
wenzelm [Wed, 18 May 2011 23:39:22 +0200] rev 43759
basic support for overpainting of text, imitating jEdit internals;

Fri, 20 May 2011 12:59:33 +0200exercise more type systems (but only sound or quasi-sound ones)
blanchet [Fri, 20 May 2011 12:59:33 +0200] rev 43758
exercise more type systems (but only sound or quasi-sound ones)

Fri, 20 May 2011 12:47:59 +0200added see also
blanchet [Fri, 20 May 2011 12:47:59 +0200] rev 43757
added see also

Fri, 20 May 2011 12:47:59 +0200document new type system and soundness properties of the different systems
blanchet [Fri, 20 May 2011 12:47:59 +0200] rev 43756
document new type system and soundness properties of the different systems

Fri, 20 May 2011 12:47:59 +0200improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet [Fri, 20 May 2011 12:47:59 +0200] rev 43755
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything

Fri, 20 May 2011 12:47:59 +0200reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts
blanchet [Fri, 20 May 2011 12:47:59 +0200] rev 43754
reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts

Fri, 20 May 2011 12:47:59 +0200more doc fiddling
blanchet [Fri, 20 May 2011 12:47:59 +0200] rev 43753
more doc fiddling