Nominal-General/nominal_library.ML
Fri, 03 Sep 2010 22:22:43 +0800 Christian Urban made the fv-definition aggree more with alpha (needed in the support proofs)
Sun, 29 Aug 2010 01:17:36 +0800 Christian Urban added proofs for fsupp properties
Sun, 29 Aug 2010 00:09:45 +0800 Christian Urban proved supports lemmas
Sat, 28 Aug 2010 13:41:31 +0800 Christian Urban updated to new Isabelle
Thu, 19 Aug 2010 18:24:36 +0800 Christian Urban used @{const_name} hopefully everywhere
Wed, 18 Aug 2010 00:19:15 +0800 Christian Urban improved runtime slightly, by constructing an explicit size measure for the function definitions
Tue, 17 Aug 2010 18:00:55 +0800 Christian Urban deleted unused code
Tue, 17 Aug 2010 17:52:25 +0800 Christian Urban improved code
Sun, 15 Aug 2010 11:03:13 +0800 Christian Urban simplified code
Sat, 14 Aug 2010 23:33:23 +0800 Christian Urban improved code
Sat, 14 Aug 2010 16:54:41 +0800 Christian Urban more experiments with lifting
Sat, 31 Jul 2010 01:24:39 +0100 Christian Urban introduced a general alpha_prove method
Tue, 27 Jul 2010 09:09:02 +0200 Christian Urban fixed order of fold_union to make alpha and fv agree
Mon, 19 Jul 2010 16:59:43 +0100 Christian Urban minor polishing
Wed, 09 Jun 2010 15:14:16 +0200 Christian Urban transitivity proofs done
less more (0) -15 tip