Nominal/Fv.thy
Tue, 16 Mar 2010 15:27:47 +0100 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings.
Tue, 16 Mar 2010 12:06:22 +0100 Cezary Kaliszyk Removed pi o bn = bn' assumption in alpha
Thu, 11 Mar 2010 20:49:31 +0100 Cezary Kaliszyk Do not fail if the finite support proof fails.
less more (0) -30 -10 -3 tip