| Fri, 20 May 2011 17:16:13 +0200 | blanchet | prevent unsound combinator proofs in partially typed polymorphic type systems | changeset | files |
| Fri, 20 May 2011 16:23:03 +0200 | hoelzl | add lemma prob_finite_product | changeset | files |
| Fri, 20 May 2011 16:22:24 +0200 | hoelzl | simp rules for empty intervals on dense linear order | changeset | files |
| Fri, 20 May 2011 14:12:59 +0200 | wenzelm | merged | changeset | files |
| Fri, 20 May 2011 12:59:33 +0200 | blanchet | exercise more type systems (but only sound or quasi-sound ones) | changeset | files |
| Fri, 20 May 2011 12:47:59 +0200 | blanchet | added see also | changeset | files |
| Fri, 20 May 2011 12:47:59 +0200 | blanchet | document new type system and soundness properties of the different systems | changeset | files |
| Fri, 20 May 2011 12:47:59 +0200 | blanchet | 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 | changeset | files |