blanchet [Fri, 20 May 2011 18:12:12 +0200] rev 43767
update example
blanchet [Fri, 20 May 2011 18:01:46 +0200] rev 43766
name tuning
blanchet [Fri, 20 May 2011 17:16:13 +0200] rev 43765
further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
blanchet [Fri, 20 May 2011 17:16:13 +0200] rev 43764
prevent unsound combinator proofs in partially typed polymorphic type systems
hoelzl [Fri, 20 May 2011 16:23:03 +0200] rev 43763
add lemma prob_finite_product
hoelzl [Fri, 20 May 2011 16:22:24 +0200] rev 43762
simp rules for empty intervals on dense linear order
wenzelm [Fri, 20 May 2011 14:12:59 +0200] rev 43761
merged
wenzelm [Fri, 20 May 2011 14:03:42 +0200] rev 43760
removed some obsolete text;
wenzelm [Wed, 18 May 2011 23:39:22 +0200] rev 43759
basic support for overpainting of text, imitating jEdit internals;
blanchet [Fri, 20 May 2011 12:59:33 +0200] rev 43758
exercise more type systems (but only sound or quasi-sound ones)