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.
Quot/Nominal/LamEx.thy
Fri, 12 Feb 2010 16:04:10 +0100 Cezary Kaliszyk renamed 'as' to 'is' everywhere. file | diff | annotate
Thu, 11 Feb 2010 14:00:00 +0100 Cezary Kaliszyk Notation available locally file | diff | annotate
Thu, 11 Feb 2010 10:06:02 +0100 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2. file | diff | annotate
Mon, 08 Feb 2010 13:12:55 +0100 Christian Urban moved some lemmas to Nominal; updated all files file | diff | annotate
Tue, 02 Feb 2010 14:55:07 +0100 Cezary Kaliszyk First experiments in Terms. file | diff | annotate
Tue, 02 Feb 2010 10:20:54 +0100 Cezary Kaliszyk General alpha_gen_trans for one-variable abstraction. file | diff | annotate
Mon, 01 Feb 2010 20:02:44 +0100 Cezary Kaliszyk merge file | diff | annotate
Mon, 01 Feb 2010 16:05:59 +0100 Cezary Kaliszyk All should be ok now. file | diff | annotate
Mon, 01 Feb 2010 18:57:39 +0100 Christian Urban repaired according to changes in Abs.thy file | diff | annotate
Mon, 01 Feb 2010 15:57:37 +0100 Cezary Kaliszyk Fixed wrong rename. file | diff | annotate
Mon, 01 Feb 2010 15:45:40 +0100 Cezary Kaliszyk Lambda based on alpha_gen, under construction. file | diff | annotate
Mon, 01 Feb 2010 09:56:32 +0100 Cezary Kaliszyk Ported LF to the generic lambda and solved the simpler _supp cases. file | diff | annotate
Sat, 30 Jan 2010 11:44:25 +0100 Christian Urban introduced a generic alpha (but not sure whether it is helpful) file | diff | annotate
Fri, 29 Jan 2010 07:09:52 +0100 Christian Urban now also final step is proved - the supp of lambdas is now completely characterised file | diff | annotate
Fri, 29 Jan 2010 00:22:00 +0100 Christian Urban the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms file | diff | annotate
Thu, 28 Jan 2010 15:47:35 +0100 Christian Urban attempt of a general abstraction operator file | diff | annotate
Thu, 28 Jan 2010 14:20:26 +0100 Christian Urban attempt to prove equivalence between alpha definitions file | diff | annotate
Thu, 28 Jan 2010 12:25:38 +0100 Cezary Kaliszyk Minor when looking at lam.distinct and lam.inject file | diff | annotate
Thu, 28 Jan 2010 01:24:09 +0100 Christian Urban test about supp/freshness for lam (old proofs work in principle - for single binders) file | diff | annotate
Tue, 26 Jan 2010 20:07:50 +0100 Christian Urban added an LamEx example together with the new nominal infrastructure file | diff | annotate
less more (0) tip
nominal2