Nominal/Ex/Classical.thy
2011-07-05 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
2011-07-05 Christian Urban added another example which seems difficult to define
2011-07-05 Christian Urban exported various FCB-lemmas to a separate file
2011-06-29 Christian Urban moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
2011-06-28 Cezary Kaliszyk Experiments with res
2011-06-27 Christian Urban proved the fcb also for sets (no restriction yet)
2011-06-27 Christian Urban streamlined the fcb-proof and made fcb1 a special case of fcb
2011-06-27 Christian Urban completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier)
2011-06-27 Christian Urban fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction.
2011-06-26 Cezary Kaliszyk equality of lst_binder and a few helper lemmas
2011-06-26 Christian Urban only one of the fcb precondistions are needed (probably the same with the perm-conditions)
2011-06-26 Christian Urban another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
2011-06-25 Christian Urban did all cases, except the multiple binder case
2011-06-25 Christian Urban an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders.
2011-06-24 Christian Urban except for the interated binder case, finished definition in Calssical.thy
2011-06-24 Cezary Kaliszyk Speed-up the completeness proof.
2011-06-23 Christian Urban the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
2011-06-23 Christian Urban expanded the example
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples
2010-08-29 Christian Urban renamed NewParser to Nominal2
2010-08-25 Christian Urban cleaned up (almost completely) the examples
2010-08-25 Christian Urban automatic lifting
2010-06-07 Christian Urban work on transitivity proof
2010-06-02 Christian Urban fixed problem with bn_info
2010-05-12 Christian Urban fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
2010-05-12 Cezary Kaliszyk include set_simps and append_simps in fv_rsp
2010-05-12 Cezary Kaliszyk Use equivariance instead of alpha_eqvt
2010-05-11 Cezary Kaliszyk Include raw permutation definitions in eqvt
2010-05-11 Cezary Kaliszyk Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
2010-05-05 Christian Urban solved the problem with equivariance by first eta-normalising the goal
2010-05-03 Cezary Kaliszyk Added cheats to classical
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-04-16 Christian Urban automatic proofs for equivariance of alphas
2010-04-08 Christian Urban properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
less more (0) tip