| Fri, 03 Apr 2009 16:17:50 +0200 |
nipkow |
Finite_Set: lemma
|
file |
diff |
annotate
|
| Fri, 03 Apr 2009 09:27:31 +0200 |
nipkow |
added setsum_eq_1_iff
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 22:29:27 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 22:29:10 +0200 |
nipkow |
cleaned up setprod_zero-related lemmas
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 11:34:21 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 11:31:24 -0700 |
huffman |
generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
|
file |
diff |
annotate
|
| Wed, 01 Apr 2009 16:03:00 +0200 |
nipkow |
added strong_setprod_cong[cong] (in analogy with setsum)
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 20:29:37 +0100 |
haftmann |
equalities for Min, Max
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 19:21:55 +0000 |
chaieb |
Added general theorems for fold_image, setsum and set_prod
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 13:39:05 +0100 |
haftmann |
reverted to previous version of Finite_Set.thy
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 11:17:29 +0000 |
paulson |
No idea what happened here!
|
file |
diff |
annotate
|
| Sun, 15 Feb 2009 22:58:02 +0100 |
nipkow |
dvd and setprod lemmas
|
file |
diff |
annotate
|
| Sun, 15 Feb 2009 16:25:16 +0100 |
nipkow |
added finite_set_choice
|
file |
diff |
annotate
|
| Sun, 15 Feb 2009 11:26:38 +0100 |
nipkow |
more finiteness
|
file |
diff |
annotate
|
| Sun, 15 Feb 2009 07:54:16 +0100 |
nipkow |
more finiteness
|
file |
diff |
annotate
|
| Sat, 14 Feb 2009 19:27:15 +0100 |
nipkow |
more finiteness
|
file |
diff |
annotate
|
| Sat, 14 Feb 2009 08:45:16 +0100 |
nipkow |
more finiteness changes
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 23:55:04 +0100 |
nipkow |
finiteness lemmas
|
file |
diff |
annotate
|
| Thu, 12 Feb 2009 18:14:43 +0100 |
nipkow |
Moved FTA into Lib and cleaned it up a little.
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 21:26:21 +0100 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
| Thu, 29 Jan 2009 09:35:51 +0000 |
chaieb |
dded theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 13:23:59 +0000 |
chaieb |
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
changed import hierarchy
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:31 +0100 |
haftmann |
dropped ID
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 15:31:38 -0800 |
huffman |
move lemmas from Numeral_Type.thy to other theories
|
file |
diff |
annotate
|