Thu, 18 May 1995 11:51:23 +0200 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp [Thu, 18 May 1995 11:51:23 +0200] rev 1123
Krzysztof Grabczewski's (nearly) complete AC proofs
Mon, 15 May 1995 09:35:07 +0200 renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.
nipkow [Mon, 15 May 1995 09:35:07 +0200] rev 1122
renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.
Sat, 13 May 1995 14:08:24 +0200 Added some lemmas about r^*.
nipkow [Sat, 13 May 1995 14:08:24 +0200] rev 1121
Added some lemmas about r^*.
Sat, 13 May 1995 13:46:48 +0200 Lambda calculus in de Bruijn notation.
nipkow [Sat, 13 May 1995 13:46:48 +0200] rev 1120
Lambda calculus in de Bruijn notation. Proof of confluence.
Thu, 11 May 1995 10:42:19 +0200 Indexing of COMP
lcp [Thu, 11 May 1995 10:42:19 +0200] rev 1119
Indexing of COMP
Thu, 11 May 1995 10:38:30 +0200 Indexing of FILTER and COND
lcp [Thu, 11 May 1995 10:38:30 +0200] rev 1118
Indexing of FILTER and COND
Thu, 11 May 1995 10:33:07 +0200 show_sorts
lcp [Thu, 11 May 1995 10:33:07 +0200] rev 1117
show_sorts
Wed, 10 May 1995 08:38:52 +0200 Modified translation for pattern abstraction.
nipkow [Wed, 10 May 1995 08:38:52 +0200] rev 1116
Modified translation for pattern abstraction.
Tue, 09 May 1995 22:10:48 +0200 Moved induct2 from Hoare to Lfp.
nipkow [Tue, 09 May 1995 22:10:48 +0200] rev 1115
Moved induct2 from Hoare to Lfp.
Tue, 09 May 1995 22:10:08 +0200 Prod is now a parent of Lfp.
nipkow [Tue, 09 May 1995 22:10:08 +0200] rev 1114
Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip