| Wed, 27 Jul 2011 19:34:30 +0200 |
hoelzl |
finite vimage on arbitrary domains
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 19:48:02 +0200 |
haftmann |
moving UNIV = ... equations to their proper theories
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:35:44 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:07:17 +0200 |
haftmann |
point-free characterization of operations on finite sets
|
file |
diff |
annotate
|
| Fri, 20 May 2011 11:44:16 +0200 |
haftmann |
names of fold_set locales resemble name of characteristic property more closely
|
file |
diff |
annotate
|
| Fri, 20 May 2011 08:16:56 +0200 |
haftmann |
use point-free characterization for locale fun_left_comm_idem
|
file |
diff |
annotate
|
| Sat, 14 May 2011 18:26:25 +0200 |
haftmann |
use pointfree characterisation for fold_set locale
|
file |
diff |
annotate
|
| Thu, 12 May 2011 11:03:48 +0200 |
haftmann |
more uniform naming of lemma
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 13:01:27 +0200 |
haftmann |
dropped unused lemmas; proper Isar proof
|
file |
diff |
annotate
|
| Sun, 03 Apr 2011 11:40:32 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 02 Apr 2011 18:07:29 +0200 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 09:58:13 +0100 |
nipkow |
tuned lemma
|
file |
diff |
annotate
|
| Wed, 16 Mar 2011 19:50:56 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 21 Jan 2011 09:44:12 +0100 |
haftmann |
moved theorem
|
file |
diff |
annotate
|
| Fri, 21 Jan 2011 09:41:59 +0100 |
haftmann |
restructured theory;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 20:38:58 +0100 |
wenzelm |
recoded latin1 as utf8;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adding code equation for finiteness of finite types
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 15:20:51 +0100 |
nipkow |
gave more standard finite set rules simp and intro attribute
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 18:06:48 +0100 |
nipkow |
new lemma
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 14:14:17 +0100 |
hoelzl |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 08:29:32 +0100 |
nipkow |
removed assumption
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 13 Aug 2010 10:51:23 +0200 |
haftmann |
import swap prevents strange failure of SML code generator for datatypes
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 11:39:27 +0200 |
haftmann |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 22:40:58 +0200 |
nipkow |
added pigeonhole lemmas
|
file |
diff |
annotate
|
| Tue, 04 May 2010 10:02:43 +0200 |
haftmann |
avoid if on rhs of default simp rules
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 11:05:11 +0200 |
Christian Urban |
simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
|
file |
diff |
annotate
|
| Tue, 30 Mar 2010 15:46:50 -0700 |
huffman |
simplify fold_graph proofs
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:59:20 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:56:32 +0100 |
haftmann |
added locales folding_one_(idem); various streamlining and tuning
|
file |
diff |
annotate
|
| Mon, 15 Mar 2010 15:13:07 +0100 |
haftmann |
corrected disastrous syntax declarations
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 14:38:13 +0100 |
haftmann |
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 16:53:27 +0100 |
haftmann |
split off theory Big_Operators from theory Finite_Set
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 17:09:44 +0100 |
hoelzl |
Generalized setsum_cases
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 14:47:01 +0100 |
haftmann |
moved remaning class operations from Algebras.thy to Groups.thy
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 17:57:37 +0100 |
hoelzl |
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:46 +0100 |
haftmann |
added lemmas involving Min, Max, uminus
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Fri, 01 Jan 2010 19:15:43 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 13:51:50 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 07:02:13 -0800 |
huffman |
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 17:05:56 +0000 |
paulson |
Two new theorems about cardinality
|
file |
diff |
annotate
|
| Sat, 05 Dec 2009 20:02:21 +0100 |
haftmann |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 11:16:57 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 10:17:43 +0100 |
nipkow |
fixed order of parameters in induction rules
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 09:27:48 +0200 |
nipkow |
inv_onto -> inv_into
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 12:07:56 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 12:07:25 +0200 |
nipkow |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2009 09:50:31 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 08:25:51 +0200 |
haftmann |
inf/sup_absorb are no default simp rules any longer
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 15:39:46 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Sat, 19 Sep 2009 07:38:03 +0200 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
file |
diff |
annotate
|
| Thu, 24 Sep 2009 18:29:29 +0200 |
haftmann |
idempotency case for fold1
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 15:36:55 +0200 |
haftmann |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 19:15:59 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 18:44:54 +0200 |
haftmann |
adapted to localized interpretation of min/max-lattice
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 08:32:07 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 15:54:19 +0200 |
haftmann |
refinement of lattice classes
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 15:09:33 +0200 |
nipkow |
More finite set induction rules
|
file |
diff |
annotate
|
| Sun, 12 Jul 2009 11:36:09 +0200 |
nipkow |
typo
|
file |
diff |
annotate
|
| Sun, 12 Jul 2009 11:25:56 +0200 |
nipkow |
resolvd conflict
|
file |
diff |
annotate
|
| Sun, 12 Jul 2009 10:14:51 +0200 |
nipkow |
More about gcd/lcm, and some cleaning up
|
file |
diff |
annotate
|
| Sat, 11 Jul 2009 21:33:01 +0200 |
haftmann |
added boolean_algebra type class; tuned lattice duals
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 21:24:32 +0200 |
wenzelm |
recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 15:48:55 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Thu, 18 Jun 2009 17:14:08 +0100 |
paulson |
Removed unnecessary conditions concerning nonzero divisors
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 11:31:27 +0200 |
haftmann |
lemma finite_image_set by Jeremy Avigad
|
file |
diff |
annotate
|
| Fri, 05 Jun 2009 13:35:33 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 05 Jun 2009 08:06:03 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 15:28:58 +0200 |
haftmann |
lemmas about basic set operations and Finite_Set.fold
|
file |
diff |
annotate
|
| Fri, 05 Jun 2009 09:54:26 +0200 |
nipkow |
new lemma
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 19:44:06 +0200 |
nipkow |
finite lemmas
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 13:26:32 +0200 |
nipkow |
A few finite lemmas
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 16:23:43 +0200 |
haftmann |
added/moved lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Sat, 09 May 2009 07:25:22 +0200 |
nipkow |
lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 15:50:30 +0200 |
haftmann |
stripped class recpower further
|
file |
diff |
annotate
|
| 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
|
| Wed, 19 Nov 2008 17:54:55 +0100 |
nipkow |
Added new fold operator and renamed the old oe to fold_image.
|
file |
diff |
annotate
|