Sun, 28 May 2017 11:32:15 +0200 |
nipkow |
added is_arg_min
|
file |
diff |
annotate
|
Sun, 28 May 2017 08:07:40 +0200 |
nipkow |
removed LeastM; is now arg_min
|
file |
diff |
annotate
|
Tue, 18 Oct 2016 07:04:08 +0200 |
haftmann |
restored document structure after theory refactoring
|
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
|
Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
Thu, 22 Sep 2016 00:12:17 +0200 |
wenzelm |
raw control symbols are superseded by Latex.embed_raw;
|
file |
diff |
annotate
|
Fri, 16 Sep 2016 21:35:19 +0200 |
wenzelm |
more symbols -- as in the printed document;
|
file |
diff |
annotate
|
Thu, 15 Sep 2016 19:31:17 +0200 |
nipkow |
adapted to listsum -> sum_list
|
file |
diff |
annotate
|
Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Tue, 19 Jan 2016 11:46:54 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Wed, 30 Dec 2015 21:05:15 +0100 |
wenzelm |
modernized Isabelle document markup;
|
file |
diff |
annotate
|
Wed, 30 Dec 2015 20:50:08 +0100 |
wenzelm |
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
|
file |
diff |
annotate
|
Sun, 27 Dec 2015 22:07:17 +0100 |
wenzelm |
discontinued ASCII replacement syntax <*>;
|
file |
diff |
annotate
|
Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
Sun, 31 Aug 2014 09:10:42 +0200 |
haftmann |
separated listsum material
|
file |
diff |
annotate
|
Fri, 18 Jul 2014 14:03:09 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Sun, 16 Feb 2014 18:39:40 +0100 |
blanchet |
folded 'Option.set' into BNF-generated 'set_option'
|
file |
diff |
annotate
|
Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
Sun, 15 Dec 2013 15:10:14 +0100 |
haftmann |
more algebraic terminology for theories about big operators
|
file |
diff |
annotate
|
Mon, 09 Dec 2013 12:22:23 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Fri, 30 Aug 2013 14:07:49 +0200 |
nipkow |
more set syntax
|
file |
diff |
annotate
|
Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
Wed, 19 Dec 2012 22:44:24 +0100 |
nipkow |
tuned infix table
|
file |
diff |
annotate
|
Mon, 17 Dec 2012 18:23:08 +0100 |
nipkow |
added table of infix operators
|
file |
diff |
annotate
|
Tue, 28 Aug 2012 18:57:32 +0200 |
wenzelm |
renamed doc-src to src/Doc;
|
file |
diff |
annotate
| base
|