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.
less more (0) -14 tip