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
|