Nominal/nominal_dt_alpha.ML
Wed, 11 Aug 2010 16:21:24 +0800 Christian Urban added a function that transforms the helper-rsp lemmas into real rsp lemmas
Sun, 08 Aug 2010 10:12:38 +0800 Christian Urban proved rsp-helper lemmas of size functions
Sat, 31 Jul 2010 02:10:42 +0100 Christian Urban tuning
Sat, 31 Jul 2010 02:05:25 +0100 Christian Urban further simplification with alpha_prove
Sat, 31 Jul 2010 01:24:39 +0100 Christian Urban introduced a general alpha_prove method
Thu, 29 Jul 2010 10:16:33 +0100 Christian Urban helper lemmas for rsp-lemmas
Tue, 27 Jul 2010 14:37:59 +0200 Christian Urban cleaned up a bit Abs.thy
Mon, 19 Jul 2010 16:59:43 +0100 Christian Urban minor polishing
Tue, 22 Jun 2010 18:07:53 +0100 Christian Urban proved eqvip theorems for alphas
Tue, 22 Jun 2010 13:05:00 +0100 Christian Urban prove that alpha implies alpha_bn (needed for rsp proofs)
Fri, 11 Jun 2010 03:02:42 +0200 Christian Urban also symmetry
Thu, 10 Jun 2010 14:53:28 +0200 Christian Urban premerge
less more (0) -12 tip