| 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
|
| Fri, 23 Dec 2011 15:55:23 +0100 |
huffman |
remove redundant lemma word_sub_def
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 09:39:14 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 17:49:42 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 23:23:51 +0100 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
| Sat, 10 Dec 2011 22:00:42 +0100 |
huffman |
prove class instances without extra lemmas
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 14:52:51 +0100 |
huffman |
remove redundant lemma word_diff_minus
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 11:31:13 +0100 |
noschinl |
more systematic lemma name
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:03 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Sun, 04 Dec 2011 13:10:19 +0100 |
huffman |
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 13:34:14 +0100 |
blanchet |
added "minimize" option for more control over automatic minimization
|
file |
diff |
annotate
|