Tue, 06 Apr 2021 18:12:20 +0000 |
haftmann |
new lemmas
|
file |
diff |
annotate
|
Sun, 15 Nov 2020 16:51:58 +0000 |
haftmann |
moved lemmas from AFP to distribution
|
file |
diff |
annotate
|
Tue, 03 Nov 2020 12:57:18 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
Fri, 21 Aug 2020 18:59:30 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Sat, 11 Jul 2020 18:09:09 +0000 |
haftmann |
a generic horner sum operation
|
file |
diff |
annotate
|
Wed, 23 Oct 2019 16:09:24 +0000 |
haftmann |
more transfer rules
|
file |
diff |
annotate
|
Wed, 23 Oct 2019 16:09:23 +0000 |
haftmann |
tuned syntax
|
file |
diff |
annotate
|
Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
Sun, 04 Nov 2018 09:57:49 +0100 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
Tue, 23 Jan 2018 12:28:46 +0100 |
Lars Hupel |
drop redundant cong rules
|
file |
diff |
annotate
|
Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
Tue, 15 Aug 2017 19:47:08 +0200 |
nipkow |
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
|
file |
diff |
annotate
|
Thu, 03 Aug 2017 09:30:09 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
Wed, 02 Aug 2017 18:22:02 +0200 |
nipkow |
generalized lemma
|
file |
diff |
annotate
|
Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
Wed, 22 Jun 2016 10:09:20 +0200 |
wenzelm |
bundle lifting_syntax;
|
file |
diff |
annotate
|
Thu, 16 Jun 2016 17:57:09 +0200 |
eberlm |
Various additions to polynomials, FPSs, Gamma function
|
file |
diff |
annotate
|
Sat, 11 Jun 2016 16:22:42 +0200 |
haftmann |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
|
file |
diff |
annotate
|
Wed, 18 May 2016 12:24:33 +0200 |
Manuel Eberl |
Resolved name clash
|
file |
diff |
annotate
|
Tue, 17 May 2016 17:05:35 +0200 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Wed, 02 Dec 2015 19:14:57 +0100 |
haftmann |
modernized
|
file |
diff |
annotate
|
Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Mon, 22 Jun 2015 11:15:23 +0200 |
nipkow |
modernized name
|
file |
diff |
annotate
|
Tue, 17 Mar 2015 09:22:17 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
Thu, 13 Nov 2014 12:35:55 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
Thu, 18 Sep 2014 15:07:43 +0200 |
haftmann |
product over monoids for lists
|
file |
diff |
annotate
|
Thu, 11 Sep 2014 23:12:32 +0200 |
haftmann |
abstract product over monoid for lists
|
file |
diff |
annotate
|
Wed, 03 Sep 2014 00:06:24 +0200 |
blanchet |
use 'datatype_new' in 'Main'
|
file |
diff |
annotate
|
Sun, 31 Aug 2014 09:10:42 +0200 |
haftmann |
separated listsum material
|
file |
diff |
annotate
|