| Sat, 15 Jun 2013 17:19:23 +0200 |
haftmann |
selection operator smallest_prime_beyond
|
file |
diff |
annotate
|
| Mon, 10 Jun 2013 20:43:17 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| 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
|