Mon, 11 Oct 2010 21:35:31 -0700 | huffman | new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI | file | diff | annotate |
Mon, 11 Oct 2010 09:54:04 -0700 | huffman | add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite | file | diff | annotate |