| Sun, 25 Oct 2009 00:00:53 +0200 |
wenzelm |
adapted Function_Lib (cf. b8cdd3d73022);
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 13:12:52 +0200 |
wenzelm |
Goal.finish: explicit context for printing;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2009 14:47:08 +0100 |
wenzelm |
avoid mixing of left/right associative infixes, to make it work with experimental Poly/ML 5.3 branch;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 15:24:18 +0100 |
wenzelm |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:56:51 +0100 |
haftmann |
HOLogic.mk_set, HOLogic.dest_set
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:11 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 08:00:24 +0200 |
haftmann |
fixed headers
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:28:21 +0200 |
wenzelm |
oops -- pr_graph = Syntax.string_of_term;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:20 +0200 |
wenzelm |
pr_matrix: proper context;
|
file |
diff |
annotate
|
| Mon, 12 May 2008 22:11:06 +0200 |
krauss |
Measure functions can now be declared via special rules, allowing for a
|
file |
diff |
annotate
|
| Sat, 01 Mar 2008 14:10:13 +0100 |
wenzelm |
use more antiquotations;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 17:44:53 +0100 |
krauss |
moved stuff about size change termination to its own session
|
file |
diff |
annotate
|