| Thu, 31 Jan 2008 11:44:43 +0100 |
haftmann |
proper term_of functions
|
changeset |
files
|
| Thu, 31 Jan 2008 09:16:01 +0100 |
haftmann |
avoiding dynamic simpset lookup
|
changeset |
files
|
| Thu, 31 Jan 2008 01:31:19 +0100 |
huffman |
new lemma is_lub_Pair; cleaned up some proofs
|
changeset |
files
|
| Wed, 30 Jan 2008 17:36:03 +0100 |
nipkow |
commented stuff out
|
changeset |
files
|
| Wed, 30 Jan 2008 17:34:21 +0100 |
nipkow |
added multiset comprehension
|
changeset |
files
|
| Wed, 30 Jan 2008 10:57:47 +0100 |
haftmann |
idempotent semigroups
|
changeset |
files
|
| Wed, 30 Jan 2008 10:57:46 +0100 |
haftmann |
dual orders and dual lattices
|
changeset |
files
|
| Wed, 30 Jan 2008 10:57:44 +0100 |
haftmann |
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
|
changeset |
files
|
| Tue, 29 Jan 2008 18:00:12 +0100 |
huffman |
new term-building combinators
|
changeset |
files
|
| Tue, 29 Jan 2008 10:20:00 +0100 |
haftmann |
cleaned up evaluation interfaces
|
changeset |
files
|
| Tue, 29 Jan 2008 10:19:58 +0100 |
haftmann |
tuned names
|
changeset |
files
|
| Tue, 29 Jan 2008 10:19:56 +0100 |
haftmann |
treating division by zero properly
|
changeset |
files
|
| Mon, 28 Jan 2008 22:27:29 +0100 |
wenzelm |
eliminated escaped white space;
|
changeset |
files
|
| Mon, 28 Jan 2008 22:27:27 +0100 |
wenzelm |
basic scanners: produce symbol list instead of imploded string;
|
changeset |
files
|
| Mon, 28 Jan 2008 22:27:27 +0100 |
wenzelm |
* Outer syntax: string tokens no longer admit escaped white space;
|
changeset |
files
|
| Mon, 28 Jan 2008 22:27:26 +0100 |
wenzelm |
location_of_position: Position.column_of (which counts Isabelle symbols, not characters);
|
changeset |
files
|