| Mon, 04 Oct 2010 06:45:57 -0700 | huffman | define is_ub predicate using bounded quantifier | file | diff | annotate |
| Fri, 01 Oct 2010 07:40:57 -0700 | huffman | added lemmas to List_Cpo.thy | file | diff | annotate |
| Thu, 30 Sep 2010 18:46:19 -0700 | huffman | rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs | file | diff | annotate |
| Mon, 13 Sep 2010 11:13:15 +0200 | nipkow | renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI | file | diff | annotate |
| Tue, 07 Sep 2010 15:56:33 -0700 | huffman | set up Nil and Cons to work as fixrec patterns | file | diff | annotate |
| Tue, 07 Sep 2010 12:04:18 +0200 | nipkow | renamed expand_*_eq in HOLCF as well | file | diff | annotate |
| Sat, 04 Sep 2010 07:26:34 -0700 | huffman | add List_Cpo.thy to HOLCF/Library | file | diff | annotate |