Nominal/Parser.thy
2010-03-11 Cezary Kaliszyk Add explicit alpha_eqvt_cheat.
2010-03-11 Cezary Kaliszyk Export tactic out of alpha_eqvt.
2010-03-10 Christian Urban merged
2010-03-10 Christian Urban almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
2010-03-10 Cezary Kaliszyk Undoing mistakenly committed parser experiments.
2010-03-10 Cezary Kaliszyk alpha_eqvt for recursive term1.
2010-03-10 Cezary Kaliszyk Linked parser to fv and alpha.
2010-03-10 Christian Urban parser produces ordered bn-fun information
2010-03-09 Christian Urban added bn-information, but it is not yet ordered according to the dts
2010-03-09 Cezary Kaliszyk A version of Fv that takes into account recursive and non-recursive bindings.
2010-03-08 Christian Urban merged
2010-03-08 Christian Urban updated to new Isabelle
2010-03-08 Cezary Kaliszyk More fine-grained nominal restriction for debugging.
2010-03-05 Cezary Kaliszyk Lift fv and bn eqvts; no need to lift alpha_eqvt.
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-03 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
2010-03-03 Cezary Kaliszyk weird eqvt
2010-03-02 Cezary Kaliszyk Comment out the part that does not work with 2 quantifiers.
2010-03-02 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Cezary Kaliszyk Working bv_eqvt
2010-03-02 Cezary Kaliszyk Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02 Christian Urban rawified the bind specs (ready to be used now)
2010-03-01 Christian Urban modified for new binding format - hope it is the intended one
2010-03-01 Christian Urban further code-refactoring in the parser
2010-03-01 Christian Urban slight simplification of the raw-decl generation
less more (0) -28 tip