Mon, 05 Nov 2007 17:48:04 +0100 | ballarin | Type instance of thm mk_left_commute in locales. | file | diff | annotate |
Tue, 21 Aug 2007 20:53:37 +0200 | huffman | declare conj_absorb [simp] | file | diff | annotate |
Mon, 20 Aug 2007 20:38:32 +0200 | huffman | cleaned up; declared more simp rules | file | diff | annotate |
Mon, 20 Aug 2007 00:22:18 +0200 | kleing | boolean algebras as locales and numbers as types by Brian Huffman | file | diff | annotate |