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 |
Sat, 02 Oct 2010 17:50:33 -0700 | huffman | minimize theory imports | changeset | files |