Tue, 30 Nov 2010 08:58:47 -0800 | huffman | simplify proof of LIMSEQ_unique | changeset | files |
Tue, 30 Nov 2010 08:35:04 -0800 | huffman | use new 'file' antiquotation for reference to Dedekind_Real.thy | changeset | files |
Tue, 30 Nov 2010 08:00:50 -0800 | huffman | merged | changeset | files |
Mon, 29 Nov 2010 14:37:40 -0800 | huffman | instance list :: (discrete_cpo) discrete_cpo; | changeset | files |