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/Nominal2_Abs.thy
Thu, 19 Apr 2018 13:57:17 +0100 Christian Urban updated to Isabelle 2016-1 default file | diff | annotate
Sat, 19 Mar 2016 21:06:48 +0000 Christian Urban updated to Isabelle 2016 Nominal2-Isabelle2016 file | diff | annotate
Thu, 09 Jul 2015 02:32:46 +0100 Christian Urban updated for Isabelle 2015 file | diff | annotate
Thu, 13 Mar 2014 09:21:31 +0000 Christian Urban updated to Isabelle changes file | diff | annotate
Sun, 13 Oct 2013 23:09:21 +0200 Christian Urban added slides file | diff | annotate
Fri, 19 Apr 2013 00:10:52 +0100 Christian Urban updated to simplifier changes file | diff | annotate
Wed, 27 Mar 2013 16:08:30 +0100 webertj Various changes to support Nominal2 commands in local contexts. file | diff | annotate
Tue, 28 Aug 2012 16:48:07 +0100 Christian Urban tuned file | diff | annotate
Sun, 15 Jul 2012 13:03:47 +0100 Christian Urban added a simproc for alpha-equivalence to the simplifier file | diff | annotate
Thu, 12 Jul 2012 10:11:32 +0100 Christian Urban streamlined definition of alpha-equivalence for single binders (used flip instead of swap) file | diff | annotate
Mon, 04 Jun 2012 21:39:51 +0100 Christian Urban added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often file | diff | annotate
Tue, 22 May 2012 14:00:59 +0200 Cezary Kaliszyk Added workaround for broken quotient_type in tip isabelle. file | diff | annotate
Tue, 10 Apr 2012 15:22:16 +0100 Christian Urban updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore) file | diff | annotate
Wed, 04 Apr 2012 06:19:38 +0100 Christian Urban updated to Isabelle version April 1 file | diff | annotate
Tue, 03 Jan 2012 11:43:27 +0000 Christian Urban updated to explicit set type constructor (post Isabelle 3rd January) file | diff | annotate
Mon, 05 Dec 2011 17:05:56 +0000 Christian Urban tiny improvement by removing one unnecessary assumption file | diff | annotate
Mon, 05 Dec 2011 15:34:12 +0000 Christian Urban tuned file | diff | annotate
Tue, 20 Sep 2011 14:44:50 +0900 Cezary Kaliszyk minor file | diff | annotate
Thu, 08 Sep 2011 13:03:19 +0100 Christian Urban more on paper file | diff | annotate
Tue, 05 Jul 2011 04:18:45 +0200 Christian Urban exported various FCB-lemmas to a separate file file | diff | annotate
Mon, 27 Jun 2011 19:15:18 +0100 Christian Urban fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction. file | diff | annotate
Mon, 20 Jun 2011 20:08:16 +0900 Cezary Kaliszyk Abs_set_fcb file | diff | annotate
Mon, 20 Jun 2011 09:59:18 +0900 Cezary Kaliszyk Move lst_fcb to Nominal2_Abs file | diff | annotate
Fri, 10 Jun 2011 15:30:09 +0900 Cezary Kaliszyk Slightly modify fcb for list1 and put in common place. file | diff | annotate
Mon, 28 Feb 2011 15:21:10 +0000 Christian Urban split the library into a basics file; merged Nominal_Eqvt into Nominal_Base file | diff | annotate
Thu, 24 Feb 2011 16:26:11 +0000 Christian Urban added a lemma about fresh_star and Abs file | diff | annotate
Tue, 01 Feb 2011 08:48:14 +0900 Cezary Kaliszyk More properties that relate abs_res and abs_set. Also abs_res with less binders. file | diff | annotate
Sun, 30 Jan 2011 12:09:23 +0900 Cezary Kaliszyk alpha_res implies alpha_set :) file | diff | annotate
Wed, 19 Jan 2011 18:56:28 +0100 Christian Urban ported some of the old proofs to serve as testcases file | diff | annotate
Wed, 19 Jan 2011 17:11:10 +0100 Christian Urban added Minimal file to test things file | diff | annotate
Tue, 18 Jan 2011 18:04:40 +0100 Christian Urban derived stronger Abs_eq_iff2 theorems file | diff | annotate
Tue, 18 Jan 2011 17:30:47 +0100 Christian Urban made alpha_abs_set_stronger1 stronger file | diff | annotate
Tue, 18 Jan 2011 22:11:49 +0900 Cezary Kaliszyk alpha_abs_set_stronger1 file | diff | annotate
Tue, 18 Jan 2011 11:02:57 +0100 Christian Urban the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions file | diff | annotate
Tue, 18 Jan 2011 06:55:18 +0100 Christian Urban modified the renaming_perm lemmas file | diff | annotate
Mon, 17 Jan 2011 12:34:11 +0000 Christian Urban moved high level code from LamTest into the main libraries. file | diff | annotate
Fri, 14 Jan 2011 14:22:25 +0000 Christian Urban strengthened renaming lemmas file | diff | annotate
Mon, 03 Jan 2011 16:19:27 +0000 Christian Urban simple cases for string rule inductions file | diff | annotate
Tue, 21 Dec 2010 10:28:08 +0000 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code file | diff | annotate
Thu, 16 Dec 2010 08:42:48 +0000 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there file | diff | annotate
Tue, 07 Dec 2010 19:16:09 +0000 Christian Urban moved general theorems into the libraries file | diff | annotate
Fri, 03 Dec 2010 13:51:07 +0000 Christian Urban updated to Isabelle 2nd December file | diff | annotate
Mon, 29 Nov 2010 08:01:09 +0000 Christian Urban isarfied some of the high-level proofs file | diff | annotate
Fri, 26 Nov 2010 19:03:23 +0000 Christian Urban completely different method fro deriving the exhaust lemma file | diff | annotate
Mon, 22 Nov 2010 16:14:47 +0900 Cezary Kaliszyk current isabelle file | diff | annotate
Sun, 14 Nov 2010 16:34:47 +0000 Christian Urban merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy file | diff | annotate | base
less more (0) tip
nominal2