Nominal/Fv.thy
2010-03-08 Cezary Kaliszyk Proper recognition of atoms and atom sets.
2010-03-08 Cezary Kaliszyk Term5 written as nominal_datatype is the recursive let.
2010-03-08 Cezary Kaliszyk Fix permutation addition.
2010-03-08 Cezary Kaliszyk Update the comments
2010-03-08 Cezary Kaliszyk Gather bindings with same binder, and generate only one permutation for them.
2010-03-04 Cezary Kaliszyk Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
2010-03-04 Cezary Kaliszyk A version that just leaves the supp/\supp goal. Obviously not true.
2010-03-04 Cezary Kaliszyk Prove symp and transp of weird without the supp /\ supp = {} assumption.
2010-03-03 Cezary Kaliszyk Code for solving symp goals with multiple existentials.
2010-03-03 Cezary Kaliszyk reflp for multiple quantifiers.
2010-03-03 Cezary Kaliszyk Add the supp intersection conditions.
2010-03-02 Cezary Kaliszyk Fixes for the fv problem and alpha problem.
2010-03-02 Cezary Kaliszyk Moving wrappers out of Lift.
2010-03-02 Cezary Kaliszyk More fixes for new alpha, the whole lift script should now work again.
2010-03-02 Cezary Kaliszyk Length fix for nested recursions.
2010-03-02 Cezary Kaliszyk Fix equivp.
2010-03-01 Cezary Kaliszyk The new alpha-equivalence and testing in Trm2 and Trm5.
2010-02-26 Cezary Kaliszyk Permutation and FV_Alpha interface change.
2010-02-25 Christian Urban moved Nominal to "toplevel"
less more (0) tip