| Fri, 24 Feb 2012 11:23:34 +0100 |
blanchet |
renamed 'try_methods' to 'try0'
|
file |
diff |
annotate
|
| Wed, 22 Feb 2012 18:08:27 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Sat, 18 Feb 2012 23:05:31 +0100 |
krauss |
NEWS
|
file |
diff |
annotate
|
| Fri, 17 Feb 2012 15:42:26 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 22:18:28 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 21:08:27 +0100 |
wenzelm |
discontinued obsolete "prems" fact;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 19:31:27 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 13:24:22 +0100 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 16:59:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 07:11:04 +0100 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
docs and news
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:28 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 11:15:36 +0100 |
bulwahn |
refreshing NEWS
|
file |
diff |
annotate
|
| Mon, 16 Jan 2012 21:50:15 +0100 |
wenzelm |
position constraints for numerals enable PIDE markup;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2012 10:48:39 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Mon, 09 Jan 2012 14:47:18 +0100 |
wenzelm |
misc tuning and reformatting;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 21:48:45 +0100 |
haftmann |
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 10:53:52 +0100 |
haftmann |
more explicit NEWS
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 10:19:49 +0100 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 20:26:01 +0100 |
wenzelm |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 18:18:39 +0100 |
wenzelm |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 12:55:37 +0100 |
huffman |
fix typos
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 12:52:23 +0100 |
huffman |
remove some duplicate lemmas
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 09:15:26 +0100 |
haftmann |
be explicit about Finite_Set.fold
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 22:17:10 +0100 |
haftmann |
NEWS: unavoidable fact renames
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 16:14:59 +0100 |
haftmann |
NEWS: `set` is now a proper type constructor
|
file |
diff |
annotate
|