| Tue, 23 Apr 2013 11:14:51 +0200 |
haftmann |
tuned: unnamed contexts, interpretation and sublocale in locale target;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 22:26:04 +0200 |
haftmann |
default implementation of multisets by list with reasonable coverage of operations on multisets
|
file |
diff |
annotate
|
| Fri, 29 Mar 2013 18:57:47 +0100 |
haftmann |
reverted slip introduced in f738e6dbd844
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 21:53:56 +0100 |
haftmann |
more uniform style for interpretation and sublocale declarations
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 20:49:57 +0100 |
haftmann |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Sun, 24 Feb 2013 20:29:13 +0100 |
haftmann |
turned example into library for comparing growth of functions
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 12:24:42 +0100 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 23:19:02 +0200 |
haftmann |
more facts on setsum and setprod
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 18:23:46 +0200 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 09:02:29 +0200 |
nipkow |
abstracted lemmas
|
file |
diff |
annotate
|
| Mon, 20 Aug 2012 08:40:18 +0200 |
nipkow |
abstracted lemma
|
file |
diff |
annotate
|
| Fri, 17 Aug 2012 08:56:08 +0200 |
nipkow |
fixed lemmas
|
file |
diff |
annotate
|
| Thu, 16 Aug 2012 15:08:42 +0200 |
nipkow |
abstracted lemmas
|
file |
diff |
annotate
|
| Wed, 15 Aug 2012 14:00:12 +0200 |
nipkow |
abstracted lemmas
|
file |
diff |
annotate
|
| Wed, 15 Aug 2012 12:56:54 +0200 |
nipkow |
Backed out changeset 6cf7a9d8bbaf
|
file |
diff |
annotate
|
| Wed, 15 Aug 2012 12:18:30 +0200 |
nipkow |
abstracted lemmas
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:40:06 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 10:27:21 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 20:15:49 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 08:15:42 +0100 |
haftmann |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file |
diff |
annotate
|
| Sun, 19 Feb 2012 15:40:58 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 13:41:41 +0100 |
haftmann |
qualified Finite_Set.fold
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 12:40:08 -0400 |
hoelzl |
removed further legacy rules from Complete_Lattices
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 16:21:48 +0200 |
noschinl |
tune simpset for Complete_Lattices
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Thu, 26 May 2011 14:12:03 +0200 |
hoelzl |
generalize setsum_cases
|
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, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
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
|
| 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
|
| Mon, 17 May 2010 18:59:59 -0700 |
huffman |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
file |
diff |
annotate
|
| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 17:58:34 +0200 |
hoelzl |
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 15:37:50 +0200 |
haftmann |
use new classes (linordered_)field_inverse_zero
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:17 +0200 |
haftmann |
class division_ring_inverse_zero
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 15:17:59 +0200 |
haftmann |
sharpened constraint (c.f. 4e7f5b22dd7d)
|
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, 23 Mar 2010 12:20:27 -0700 |
huffman |
sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
|
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:31 +0100 |
haftmann |
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
|
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
| base
|