| Sun, 10 Oct 2010 16:34:20 +0200 | nipkow | simplified proof | changeset | files |
| Sun, 10 Oct 2010 18:42:13 +0700 | blanchet | avoid generating several formulas with the same name ("tfrees") | changeset | files |
| 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 |