Nominal/Fv.thy
Tue, 09 Mar 2010 16:57:51 +0100 Cezary Kaliszyk Separate primrecs in Fv.
Tue, 09 Mar 2010 16:24:39 +0100 Cezary Kaliszyk A version of Fv that takes into account recursive and non-recursive bindings.
Mon, 08 Mar 2010 15:28:25 +0100 Cezary Kaliszyk Proper recognition of atoms and atom sets.
Mon, 08 Mar 2010 14:31:04 +0100 Cezary Kaliszyk Term5 written as nominal_datatype is the recursive let.
Mon, 08 Mar 2010 11:10:43 +0100 Cezary Kaliszyk Fix permutation addition.
Mon, 08 Mar 2010 10:33:55 +0100 Cezary Kaliszyk Update the comments
Mon, 08 Mar 2010 10:08:31 +0100 Cezary Kaliszyk Gather bindings with same binder, and generate only one permutation for them.
less more (0) -10 -7 tip