Thu, 25 Aug 2011 14:25:07 +0200 | blanchet | avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics | changeset | files |
Thu, 25 Aug 2011 14:25:06 +0200 | blanchet | fixed bang encoding detection of which types to encode | changeset | files |
Thu, 25 Aug 2011 14:06:34 +0200 | krauss | lemma Compl_insert: "- insert x A = (-A) - {x}" | changeset | files |