2010-03-08 Cezary Kaliszyk More fine-grained nominal restriction for debugging.
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-08 Cezary Kaliszyk Undo effects of simp.
2010-03-07 Christian Urban merged
2010-03-07 Christian Urban updated to renamings in Isabelle
2010-03-04 Christian Urban merged
2010-03-04 Christian Urban merged
2010-03-04 Christian Urban more proofs in Abs and work on Core Haskell
2010-03-03 Christian Urban added a lemma that permutations can be represented as sums of swapping
2010-03-05 Cezary Kaliszyk Still unable to show supp=fv for let with one existential.
2010-03-05 Cezary Kaliszyk Ported LF to the parser interface.
2010-03-05 Cezary Kaliszyk merge
2010-03-05 Cezary Kaliszyk Lift fv and bn eqvts; no need to lift alpha_eqvt.
2010-03-05 Cezary Kaliszyk Not much progress about the single existential let case.
2010-03-05 Cezary Kaliszyk Fixed LF for one quantifier over 2 premises.
2010-03-05 Cezary Kaliszyk Trying to fix the proofs for the single existential... So far failed.
2010-03-04 Cezary Kaliszyk Lift distinct.
2010-03-04 Cezary Kaliszyk Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
2010-03-04 Cezary Kaliszyk Lift BV,FV,Permutations and injection :).
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 merge
2010-03-03 Cezary Kaliszyk Experiments with proving weird transp
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 Christian Urban fixed mess in Test.thy
2010-03-03 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
2010-03-03 Christian Urban only tuned
2010-03-03 Christian Urban merged
2010-03-03 Christian Urban start of paper - does not compile yet
2010-03-03 Christian Urban added ACM style file for ICFP
2010-03-03 Cezary Kaliszyk weird eqvt
2010-03-03 Cezary Kaliszyk Add the supp intersection conditions.
2010-03-02 Cezary Kaliszyk Comment out the part that does not work with 2 quantifiers.
2010-03-02 Cezary Kaliszyk Fixes for the fv problem and alpha problem.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban preliinary test about alpha-weirdo
2010-03-02 Christian Urban Another problem with permutations in alpha and possibly also in fv
2010-03-02 Christian Urban potential problem with the phd-example, where two permutations are generated, but only one is used
2010-03-02 Cezary Kaliszyk Some tests around Term4. Not sure how to fix the generated fv function.
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Cezary Kaliszyk Add image_eqvt and atom_eqvt to eqvt bases.
2010-03-02 Cezary Kaliszyk Include the raw eqvt lemmas.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban added some more examples from Peter Sewell's bestiary
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Minor
2010-03-02 Cezary Kaliszyk Working bv_eqvt
2010-03-02 Cezary Kaliszyk Moving wrappers out of Lift.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban added distinctness of perms
2010-03-02 Christian Urban updated (added lemma about commuting permutations)
2010-03-02 Cezary Kaliszyk Change type schemes to name set.
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.
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 tip