Thu, 19 Feb 2009 12:26:32 -0800 | huffman | add rule for minus 1 at type bit | changeset | files |
Thu, 19 Feb 2009 12:03:31 -0800 | huffman | add formalization of a type of integers mod 2 to Library | changeset | files |
Thu, 19 Feb 2009 09:42:23 -0800 | huffman | new theory of real inner product spaces | changeset | files |
Thu, 19 Feb 2009 09:39:49 -0800 | huffman | add Powerdomain_ex.thy | changeset | files |
Thu, 19 Feb 2009 08:07:52 -0800 | huffman | add more ordering lemmas | changeset | files |
Thu, 19 Feb 2009 06:47:06 -0800 | huffman | avoid using ab_semigroup_idem_mult locale for powerdomains | changeset | files |