Sat, 17 Oct 2009 12:31:48 +0200 |
Cezary Kaliszyk |
Merged
|
changeset |
files
|
Sat, 17 Oct 2009 12:31:36 +0200 |
Cezary Kaliszyk |
Simplified
|
changeset |
files
|
Sat, 17 Oct 2009 12:20:56 +0200 |
Cezary Kaliszyk |
Further in the proof
|
changeset |
files
|
Sat, 17 Oct 2009 11:54:50 +0200 |
Cezary Kaliszyk |
compose_tac works with the full instantiation.
|
changeset |
files
|
Sat, 17 Oct 2009 12:19:06 +0200 |
Christian Urban |
slightly simplified get_fun function
|
changeset |
files
|
Sat, 17 Oct 2009 10:40:54 +0200 |
Cezary Kaliszyk |
The instantiated version is the same modulo beta
|
changeset |
files
|
Sat, 17 Oct 2009 10:07:52 +0200 |
Cezary Kaliszyk |
Fully manually instantiated. Still fails...
|
changeset |
files
|
Sat, 17 Oct 2009 09:04:24 +0200 |
Cezary Kaliszyk |
Little progress with match/instantiate
|
changeset |
files
|
Fri, 16 Oct 2009 19:21:05 +0200 |
Cezary Kaliszyk |
Fighting with the instantiation
|
changeset |
files
|
Fri, 16 Oct 2009 17:05:52 +0200 |
Cezary Kaliszyk |
Symmetric version of REP_ABS_RSP
|
changeset |
files
|
Fri, 16 Oct 2009 16:51:01 +0200 |
Cezary Kaliszyk |
Progressing with the proof
|
changeset |
files
|
Fri, 16 Oct 2009 10:54:31 +0200 |
Cezary Kaliszyk |
Finally fix get_fun.
|
changeset |
files
|
Fri, 16 Oct 2009 08:48:56 +0200 |
Cezary Kaliszyk |
A fix for one fun_map; doesn't work for more.
|
changeset |
files
|
Fri, 16 Oct 2009 03:26:54 +0200 |
Christian Urban |
fixed the problem with function types; but only type_of works; cterm_of does not work
|
changeset |
files
|
Thu, 15 Oct 2009 16:51:24 +0200 |
Cezary Kaliszyk |
Description of the problem with get_fun.
|
changeset |
files
|