| Fri, 20 Jun 2008 19:59:00 +0200 | huffman | moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale | changeset | files |
| Fri, 20 Jun 2008 19:57:45 +0200 | huffman | add lemma Abs_image | changeset | files |
| Fri, 20 Jun 2008 18:03:01 +0200 | huffman | added some lemmas; reorganized into sections; tuned proofs | changeset | files |
| Fri, 20 Jun 2008 18:00:55 +0200 | huffman | added some lemmas; tuned proofs | changeset | files |
| Fri, 20 Jun 2008 17:58:16 +0200 | huffman | tuned | changeset | files |
| Fri, 20 Jun 2008 17:56:00 +0200 | huffman | replace less_lift with flat_less_iff | changeset | files |
| Fri, 20 Jun 2008 17:43:16 +0200 | huffman | tweak lemmas adm_all and adm_ball | changeset | files |
| Thu, 19 Jun 2008 22:50:58 +0200 | huffman | move lemmas into locales; | changeset | files |