Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Term5.thy
Mon, 22 Mar 2010 17:21:27 +0100 Cezary Kaliszyk Got rid of alpha_bn_rsp_cheat. file | diff | annotate
Mon, 22 Mar 2010 15:27:01 +0100 Cezary Kaliszyk alpha_bn_rsp_pre automatized. file | diff | annotate
Wed, 17 Mar 2010 18:52:59 +0100 Cezary Kaliszyk compose_sym2 works also for term5 file | diff | annotate
Wed, 17 Mar 2010 11:11:25 +0100 Cezary Kaliszyk Finished all proofs in Term5 and Term5n. file | diff | annotate
Tue, 16 Mar 2010 20:07:13 +0100 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not. file | diff | annotate
Tue, 16 Mar 2010 18:18:08 +0100 Cezary Kaliszyk The old recursive alpha works fine. file | diff | annotate
Tue, 16 Mar 2010 17:11:32 +0100 Cezary Kaliszyk Alpha is wrong. file | diff | annotate
Tue, 16 Mar 2010 16:17:05 +0100 Cezary Kaliszyk alpha5_transp and equivp file | diff | annotate
Tue, 16 Mar 2010 15:38:14 +0100 Cezary Kaliszyk alpha5_symp proved. file | diff | annotate
Tue, 16 Mar 2010 15:27:47 +0100 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings. file | diff | annotate
Tue, 16 Mar 2010 12:08:37 +0100 Cezary Kaliszyk The proof in 'Test' gets simpler. file | diff | annotate
Thu, 11 Mar 2010 14:09:54 +0100 Cezary Kaliszyk looking at trm5_equivp file | diff | annotate
Thu, 11 Mar 2010 13:44:54 +0100 Cezary Kaliszyk The alpha5_eqvt tactic works if I manage to build the goal. file | diff | annotate
Wed, 10 Mar 2010 16:58:14 +0100 Cezary Kaliszyk More tries about the proofs in trm5 file | diff | annotate
Wed, 10 Mar 2010 15:40:15 +0100 Cezary Kaliszyk alpha_equivp for trm5 file | diff | annotate
Wed, 10 Mar 2010 14:47:04 +0100 Cezary Kaliszyk Looking at alpha_eqvt for term5, not much progress. file | diff | annotate
Wed, 10 Mar 2010 11:39:28 +0100 Cezary Kaliszyk Testing equalities in trm5, all seems good. file | diff | annotate
Mon, 01 Mar 2010 16:04:03 +0100 Cezary Kaliszyk The new alpha-equivalence and testing in Trm2 and Trm5. file | diff | annotate
Mon, 01 Mar 2010 14:26:14 +0100 Christian Urban slight simplification of the raw-decl generation file | diff | annotate
Mon, 01 Mar 2010 11:40:48 +0100 Cezary Kaliszyk Example that shows that current alpha is wrong. file | diff | annotate
Fri, 26 Feb 2010 13:57:43 +0100 Cezary Kaliszyk Permutation and FV_Alpha interface change. file | diff | annotate
Thu, 25 Feb 2010 14:14:08 +0100 Cezary Kaliszyk Split Terms into separate files and add them to tests. file | diff | annotate
less more (0) tip
nominal2