Thu, 01 Sep 2011 16:16:25 +0900 | Cezary Kaliszyk | HOL/Import: observe distinction between sets and predicates (where possible) | changeset | files |
Wed, 31 Aug 2011 13:28:29 -0700 | huffman | simplify/generalize some proofs | changeset | files |
Wed, 31 Aug 2011 10:42:31 -0700 | huffman | generalize lemma isCont_vec_nth | changeset | files |
Wed, 31 Aug 2011 10:24:29 -0700 | huffman | convert proof to Isar-style | changeset | files |
Wed, 31 Aug 2011 13:51:22 -0700 | huffman | remove redundant lemma card_enum | changeset | files |
Wed, 31 Aug 2011 08:11:47 -0700 | huffman | move lemmas from Topology_Euclidean_Space to Euclidean_Space | changeset | files |
Wed, 31 Aug 2011 07:51:55 -0700 | huffman | convert to Isar-style proof | changeset | files |
Wed, 31 Aug 2011 13:22:50 +0200 | blanchet | make SML/NJ happy | changeset | files |