Nominal/NewParser.thy
2010-05-03 Cezary Kaliszyk Introduce eq_iff_simp to match the one from Parser.
2010-05-03 Cezary Kaliszyk Cheat support equations in new parser
2010-05-03 Cezary Kaliszyk Add explicit cheats in NewParser and comment out the examples for outside use.
2010-05-03 Cezary Kaliszyk Fix Datatype_Aux calls in NewParser.
2010-05-02 Christian Urban tried to add some comments in the huge(!) nominal2_cmd function
2010-05-02 Christian Urban attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
2010-05-01 Christian Urban merged
2010-05-01 Christian Urban tuned
2010-04-30 Cezary Kaliszyk NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
2010-04-30 Cezary Kaliszyk Merged nominal_datatype into NewParser until eqvts
2010-04-30 Cezary Kaliszyk more parser/new parser synchronization.
2010-04-30 Cezary Kaliszyk Change signature of fv and alpha generation.
2010-04-29 Cezary Kaliszyk New Alpha.
2010-04-29 Cezary Kaliszyk Fixing the definitions in the Parser.
2010-04-29 Cezary Kaliszyk Include support of unknown datatypes in new fv
2010-04-28 Christian Urban simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
2010-04-28 Christian Urban use sort at_base instead of at
2010-04-27 Christian Urban added some further problemetic tests
2010-04-27 Christian Urban some tuning
2010-04-27 Cezary Kaliszyk Rewrote FV code and included the function package.
2010-04-25 Christian Urban added definition of raw-permutations to the new-parser
2010-04-25 Christian Urban tuned
2010-04-24 Christian Urban slight tuning
2010-04-24 Christian Urban added a comment about a function where I am not sure who wrote it.
2010-04-24 Christian Urban merged
less more (0) tip