Fri, 22 Oct 2010 07:44:34 -0700 | huffman | direct instantiation unit :: discrete_cpo | changeset | files |
Fri, 22 Oct 2010 06:58:45 -0700 | huffman | remove finite_po class | changeset | files |
Fri, 22 Oct 2010 06:08:51 -0700 | huffman | simplify proofs about flift; remove unneeded lemmas | changeset | files |
Fri, 22 Oct 2010 05:54:54 -0700 | huffman | simplify proof | changeset | files |
Thu, 21 Oct 2010 15:21:39 -0700 | huffman | minimize imports | changeset | files |
Thu, 21 Oct 2010 15:19:07 -0700 | huffman | add type annotation to avoid warning | changeset | files |
Thu, 21 Oct 2010 12:51:36 -0700 | huffman | simplify some proofs, convert to Isar style | changeset | files |