| Thu, 21 Apr 2005 22:04:01 +0200 |
wenzelm |
removed;
|
changeset |
files
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
changeset |
files
|
| Thu, 21 Apr 2005 22:00:28 +0200 |
wenzelm |
adapt theories and ML files to new CPure/Pure arrangement;
|
changeset |
files
|
| Thu, 21 Apr 2005 19:16:19 +0200 |
berghofe |
Adapted use command to new behaviour of Toplevel.node_trans
|
changeset |
files
|
| Thu, 21 Apr 2005 19:13:03 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
changeset |
files
|
| Thu, 21 Apr 2005 19:12:03 +0200 |
berghofe |
- Eliminated nodup_vars check.
|
changeset |
files
|
| Thu, 21 Apr 2005 19:02:54 +0200 |
berghofe |
Moved cterm_fun from Thm to Drule.
|
changeset |
files
|
| Thu, 21 Apr 2005 18:58:44 +0200 |
berghofe |
Modified variable index in proof (necessary due to changes in the kernel).
|
changeset |
files
|
| Thu, 21 Apr 2005 18:57:18 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
changeset |
files
|
| Thu, 21 Apr 2005 18:56:03 +0200 |
berghofe |
Made inst1_tac more robust against changes of variable indices.
|
changeset |
files
|
| Thu, 21 Apr 2005 17:22:23 +0200 |
nipkow |
fix
|
changeset |
files
|
| Thu, 21 Apr 2005 17:22:17 +0200 |
nipkow |
tuning locales
|
changeset |
files
|