| Wed, 08 Jul 2009 06:42:35 +0200 |
nipkow |
name fixed
|
changeset |
files
|
| Tue, 07 Jul 2009 21:26:08 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 07 Jul 2009 17:50:03 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 07 Jul 2009 17:21:27 +0200 |
haftmann |
tuned interface of structure Code
|
changeset |
files
|
| Tue, 07 Jul 2009 17:21:26 +0200 |
haftmann |
more accurate certificates for constant aliasses
|
changeset |
files
|
| Tue, 07 Jul 2009 21:24:55 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 07 Jul 2009 17:37:00 +0200 |
haftmann |
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
|
changeset |
files
|
| Tue, 07 Jul 2009 20:16:06 +0200 |
wenzelm |
fixed proof (cf. 40501bb2d57c);
|
changeset |
files
|
| Tue, 07 Jul 2009 17:39:51 +0200 |
nipkow |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
changeset |
files
|
| Tue, 07 Jul 2009 07:56:24 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 06 Jul 2009 16:49:51 +0200 |
haftmann |
tuned code
|
changeset |
files
|
| Mon, 06 Jul 2009 14:19:13 +0200 |
haftmann |
moved Inductive.myinv to Fun.inv; tuned
|
changeset |
files
|
| Tue, 07 Jul 2009 00:29:34 +0200 |
wenzelm |
add_classrel/arity: strip_shyps of stored result;
|
changeset |
files
|
| Mon, 06 Jul 2009 22:42:27 +0200 |
wenzelm |
clarified strip_shyps: proper type witnesses for present sorts;
|
changeset |
files
|
| Mon, 06 Jul 2009 22:41:00 +0200 |
wenzelm |
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
|
changeset |
files
|