LFex.thy
Thu, 03 Dec 2009 11:28:19 +0100 Cezary Kaliszyk Included all_prs and ex_prs in the lambda_prs conversion.
Wed, 02 Dec 2009 23:31:30 +0100 Christian Urban deleted now obsolete argument rty everywhere
Wed, 02 Dec 2009 11:30:40 +0100 Cezary Kaliszyk Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Tue, 01 Dec 2009 12:16:45 +0100 Cezary Kaliszyk Cleaning 'aps'.
Mon, 30 Nov 2009 15:32:14 +0100 Cezary Kaliszyk clean_tac rewrites the definitions the other way
Mon, 30 Nov 2009 11:53:20 +0100 Cezary Kaliszyk Code cleaning.
Mon, 30 Nov 2009 02:05:22 +0100 Cezary Kaliszyk Added another induction to LFex
less more (0) -10 -7 tip