| Fri, 23 Feb 2007 08:39:27 +0100 |
haftmann |
proper treatment of -> as type constructor
|
changeset |
files
|
| Fri, 23 Feb 2007 08:39:26 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 23 Feb 2007 08:39:25 +0100 |
haftmann |
add_path for naming in proof contexts
|
changeset |
files
|
| Fri, 23 Feb 2007 08:39:24 +0100 |
haftmann |
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
|
changeset |
files
|
| Fri, 23 Feb 2007 08:39:23 +0100 |
haftmann |
slightly tuned
|
changeset |
files
|
| Fri, 23 Feb 2007 08:39:22 +0100 |
haftmann |
slight cleanup
|
changeset |
files
|
| Fri, 23 Feb 2007 08:39:21 +0100 |
haftmann |
adjusted code lemmas
|
changeset |
files
|
| Fri, 23 Feb 2007 08:39:20 +0100 |
haftmann |
continued
|
changeset |
files
|
| Fri, 23 Feb 2007 08:39:19 +0100 |
haftmann |
dropped diagnostic switch
|
changeset |
files
|
| Thu, 22 Feb 2007 10:25:14 +0100 |
paulson |
Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses
|
changeset |
files
|
| Wed, 21 Feb 2007 13:51:12 +0100 |
krauss |
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
|
changeset |
files
|
| Wed, 21 Feb 2007 02:30:06 +0100 |
kleing |
prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)
|
changeset |
files
|
| Tue, 20 Feb 2007 00:53:18 +0100 |
kleing |
added missing \
|
changeset |
files
|
| Tue, 20 Feb 2007 00:23:58 +0100 |
kleing |
updated docs with new with_dups syntax for find_theorems
|
changeset |
files
|