Fri, 18 Jan 2013 20:00:59 +0100 | hoelzl | tune prove compact_eq_totally_bounded | changeset | files |
Thu, 17 Jan 2013 15:28:53 -0800 | huffman | generalized theorem edelstein_fix to class metric_space | changeset | files |
Fri, 18 Jan 2013 16:06:45 +0100 | blanchet | tuning | changeset | files |
Fri, 18 Jan 2013 14:33:16 +0100 | blanchet | pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier | changeset | files |