Nominal/Fv.thy
Thu, 11 Mar 2010 11:41:27 +0100 Cezary Kaliszyk Proper error message.
Thu, 11 Mar 2010 11:25:56 +0100 Cezary Kaliszyk Remove tracing from fv/alpha.
Wed, 10 Mar 2010 13:29:12 +0100 Cezary Kaliszyk Allows multiple bindings with same lhs.
Wed, 10 Mar 2010 12:53:30 +0100 Cezary Kaliszyk A minor fix for shallow binders. LF works again.
Wed, 10 Mar 2010 11:19:59 +0100 Cezary Kaliszyk Fv&Alpha seem to work.
Wed, 10 Mar 2010 10:47:21 +0100 Cezary Kaliszyk include alpha in the definitions.
Wed, 10 Mar 2010 10:11:20 +0100 Cezary Kaliszyk Filled the algorithm for alpha_bn_arg
Wed, 10 Mar 2010 09:58:43 +0100 Cezary Kaliszyk rhs of alpha_bn, and template for the arguments.
Wed, 10 Mar 2010 09:45:38 +0100 Cezary Kaliszyk alpha_bn_constr template
Wed, 10 Mar 2010 09:36:07 +0100 Cezary Kaliszyk exported template for alpha_bn
Wed, 10 Mar 2010 09:09:52 +0100 Cezary Kaliszyk Use alpha_bns in normal alpha defs.
Wed, 10 Mar 2010 08:44:19 +0100 Cezary Kaliszyk alpha_bn_frees
Tue, 09 Mar 2010 21:22:22 +0100 Cezary Kaliszyk Separate lists for separate constructors, to match bn_eqs.
Tue, 09 Mar 2010 17:02:29 +0100 Cezary Kaliszyk Fix to get old alpha.
less more (0) -14 tip