| Tue, 17 Feb 2009 20:41:36 +0000 | chaieb | fixed selection of premises | changeset | files |
| Thu, 19 Feb 2009 23:18:28 -0800 | huffman | cleaned up | changeset | files |
| Thu, 19 Feb 2009 18:16:19 -0800 | huffman | declare of_int_number_of_eq [simp] | changeset | files |
| Thu, 19 Feb 2009 17:13:35 -0800 | huffman | fix case_names | changeset | files |
| Thu, 19 Feb 2009 17:11:12 -0800 | huffman | nicer induction/cases rules for numeral types | changeset | files |
| Thu, 19 Feb 2009 16:51:46 -0800 | huffman | number_ring instances for numeral types | changeset | files |
| Thu, 19 Feb 2009 12:37:03 -0800 | huffman | declare xor_compl_{left,right} [simp] | changeset | files |
| 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 |
| Thu, 19 Feb 2009 05:50:26 -0800 | huffman | merged | changeset | files |
| Wed, 18 Feb 2009 20:53:58 -0800 | huffman | add header | changeset | files |
| Wed, 18 Feb 2009 20:14:45 -0800 | huffman | move Polynomial.thy to Library | changeset | files |