LamEx.thy
Tue, 03 Nov 2009 14:04:21 +0100 Cezary Kaliszyk Preparing infrastructure for general FORALL_PRS
Mon, 02 Nov 2009 14:57:56 +0100 Cezary Kaliszyk Optimization
Mon, 02 Nov 2009 11:51:50 +0100 Cezary Kaliszyk Map does not fully work yet.
Mon, 02 Nov 2009 11:15:26 +0100 Cezary Kaliszyk Fixed quotdata_lookup.
Sat, 31 Oct 2009 11:20:55 +0100 Cezary Kaliszyk Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Fri, 30 Oct 2009 19:03:53 +0100 Cezary Kaliszyk Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Fri, 30 Oct 2009 18:31:06 +0100 Cezary Kaliszyk Regularization
Fri, 30 Oct 2009 16:35:43 +0100 Christian Urban added some facts about fresh and support of lam
Fri, 30 Oct 2009 15:52:47 +0100 Cezary Kaliszyk Lemmas about fv.
Fri, 30 Oct 2009 15:35:42 +0100 Christian Urban changed the order of rfv and reformulated a3 with rfv
Fri, 30 Oct 2009 15:32:04 +0100 Christian Urban merged
Fri, 30 Oct 2009 15:28:44 +0100 Christian Urban added fv-function
Fri, 30 Oct 2009 15:22:59 +0100 Cezary Kaliszyk The proper real_alpha
Fri, 30 Oct 2009 12:22:03 +0100 Cezary Kaliszyk Cleaning also in Lam
Thu, 29 Oct 2009 17:35:03 +0100 Cezary Kaliszyk Tried manually lifting real_alpha
Thu, 29 Oct 2009 13:30:11 +0100 Cezary Kaliszyk More tests in Lam
Thu, 29 Oct 2009 08:46:34 +0100 Cezary Kaliszyk Lifting of the 3 lemmas in LamEx
Thu, 29 Oct 2009 08:06:49 +0100 Cezary Kaliszyk Fixed wrong CARD definition and removed the "Does not work anymore" comment.
Thu, 29 Oct 2009 07:29:12 +0100 Christian Urban merged
Wed, 28 Oct 2009 19:36:52 +0100 Christian Urban fixed the definition of alpha; this *breaks* some of the experiments
Wed, 28 Oct 2009 18:08:38 +0100 Cezary Kaliszyk disambiguate ===> syntax
Wed, 28 Oct 2009 17:38:37 +0100 Cezary Kaliszyk More cleaning in Lam code
Wed, 28 Oct 2009 16:48:57 +0100 Cezary Kaliszyk Some cleaning
Wed, 28 Oct 2009 16:05:59 +0100 Cezary Kaliszyk Fixes
Wed, 28 Oct 2009 15:25:36 +0100 Christian Urban merged
Wed, 28 Oct 2009 15:25:11 +0100 Christian Urban added infrastructure for defining lifted constants
Wed, 28 Oct 2009 14:59:24 +0100 Cezary Kaliszyk First experiments with Lambda
Tue, 27 Oct 2009 14:14:30 +0100 Christian Urban added equiv-thm to the quot_info
Tue, 27 Oct 2009 11:43:02 +0100 Christian Urban added an example about lambda-terms
less more (0) tip