| Fri, 20 Jun 2008 21:00:22 +0200 | haftmann | DatatypeProp.make_distincts: only one half of each symmetric pair is constructed | changeset | files |
| Fri, 20 Jun 2008 21:00:21 +0200 | haftmann | streamlined definitions | changeset | files |
| Fri, 20 Jun 2008 21:00:16 +0200 | haftmann | moved Float.thy to Library | changeset | files |
| Fri, 20 Jun 2008 20:03:13 +0200 | huffman | removed SetPcpo.thy and cpo instance for type bool; | changeset | files |
| 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 |