Wed, 03 Nov 2010 15:57:39 -0700 | huffman | add lemma eq_imp_below | changeset | files |
Wed, 03 Nov 2010 15:47:46 -0700 | huffman | discontinue a bunch of legacy theorem names | changeset | files |
Wed, 03 Nov 2010 15:31:24 -0700 | huffman | move a few admissibility lemmas into FOCUS/Stream_adm.thy | changeset | files |
Wed, 03 Nov 2010 15:03:16 -0700 | huffman | simplify some proofs | changeset | files |