| 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
|
| Wed, 18 Feb 2009 19:51:39 -0800 |
huffman |
move FrechetDeriv.thy to Library
|
changeset |
files
|
| Wed, 18 Feb 2009 19:32:26 -0800 |
huffman |
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
|
changeset |
files
|