Sat, 17 Oct 2009 12:19:06 +0200 Christian Urban slightly simplified get_fun function
Sat, 17 Oct 2009 10:40:54 +0200 Cezary Kaliszyk The instantiated version is the same modulo beta
Sat, 17 Oct 2009 10:07:52 +0200 Cezary Kaliszyk Fully manually instantiated. Still fails...
Sat, 17 Oct 2009 09:04:24 +0200 Cezary Kaliszyk Little progress with match/instantiate
Fri, 16 Oct 2009 19:21:05 +0200 Cezary Kaliszyk Fighting with the instantiation
Fri, 16 Oct 2009 17:05:52 +0200 Cezary Kaliszyk Symmetric version of REP_ABS_RSP
Fri, 16 Oct 2009 16:51:01 +0200 Cezary Kaliszyk Progressing with the proof
Fri, 16 Oct 2009 10:54:31 +0200 Cezary Kaliszyk Finally fix get_fun.
Fri, 16 Oct 2009 08:48:56 +0200 Cezary Kaliszyk A fix for one fun_map; doesn't work for more.
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
Thu, 15 Oct 2009 16:51:24 +0200 Cezary Kaliszyk Description of the problem with get_fun.
Thu, 15 Oct 2009 16:36:20 +0200 Cezary Kaliszyk A proper build_goal_term function.
Thu, 15 Oct 2009 12:06:00 +0200 Cezary Kaliszyk Cleaning the code
Thu, 15 Oct 2009 11:57:33 +0200 Cezary Kaliszyk Merged
Thu, 15 Oct 2009 11:56:30 +0200 Cezary Kaliszyk Cleaning the proofs
(0) -100 -15 +15 +100 +300 +1000 +3000 tip