| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
rationalize imports
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 22:48:12 +0200 |
wenzelm |
prefer plain subscript for notation;
|
file |
diff |
annotate
|
| 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
|