Wed, 10 Nov 2010 08:18:32 -0800 | huffman | add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a) | changeset | files |
Wed, 10 Nov 2010 06:02:37 -0800 | huffman | instance prod :: (predomain, predomain) predomain | changeset | files |
Tue, 09 Nov 2010 19:37:11 -0800 | huffman | adapt isodefl proof script to unpointed types | changeset | files |