| Sat, 03 Feb 2007 23:42:55 +0100 |
urbanc |
added the two renaming functions from my PhD
|
changeset |
files
|
| Fri, 02 Feb 2007 17:16:16 +0100 |
urbanc |
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
|
changeset |
files
|
| Fri, 02 Feb 2007 15:47:58 +0100 |
nipkow |
a few additions and deletions
|
changeset |
files
|
| Thu, 01 Feb 2007 20:59:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Feb 2007 20:40:34 +0100 |
wenzelm |
proper use of PureThy.has_name_hint instead of hard-wired string'';
|
changeset |
files
|
| Thu, 01 Feb 2007 20:40:17 +0100 |
wenzelm |
removed non-modular comment;
|
changeset |
files
|
| Thu, 01 Feb 2007 13:41:19 +0100 |
paulson |
new theorem int_infinite
|
changeset |
files
|
| Wed, 31 Jan 2007 20:07:40 +0100 |
aspinall |
Fix tell_thm_deps to match changse in PureThy.
|
changeset |
files
|
| Wed, 31 Jan 2007 20:06:24 +0100 |
aspinall |
Expose hard-wired string which was changed and broke Proof General.
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:17 +0100 |
haftmann |
clarified error message
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:16 +0100 |
haftmann |
clarified command annotation
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:14 +0100 |
haftmann |
changed cong alist - now using AList operations instead of overwrite_warn
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:13 +0100 |
haftmann |
dropped Output.update_warn
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:12 +0100 |
haftmann |
print translation for record types with empty-sorted type variables raise Match instead of producing an error
|
changeset |
files
|
| Wed, 31 Jan 2007 16:05:10 +0100 |
haftmann |
dropped lemma duplicates in HOL.thy
|
changeset |
files
|