Wed, 06 Oct 2010 10:49:27 -0700 | huffman | major reorganization/simplification of HOLCF type classes: | changeset | files |
Tue, 05 Oct 2010 17:53:00 -0700 | Brian Huffman | add lemma finite_deflation_intro | changeset | files |
Tue, 05 Oct 2010 17:36:45 -0700 | Brian Huffman | add lemmas finite_deflation_imp_compact, cast_below_cast_iff | changeset | files |
Tue, 05 Oct 2010 17:32:02 -0700 | Brian Huffman | move lemmas to Deflation.thy | changeset | files |
Tue, 05 Oct 2010 17:07:57 -0700 | Brian Huffman | simplify proofs of powerdomain inequalities | changeset | files |
Mon, 04 Oct 2010 06:58:37 -0700 | huffman | new lemmas about lub | changeset | files |
Mon, 04 Oct 2010 06:45:57 -0700 | huffman | define is_ub predicate using bounded quantifier | changeset | files |