Nominal/Ex/AuxNoFCB.thy
2012-04-02 Cezary Kaliszyk remove smt calls
2012-03-30 Cezary Kaliszyk More cleaning
2012-03-30 Cezary Kaliszyk Clean the proof of Aux
2012-03-30 Cezary Kaliszyk Finish all subgoals about Aux.
2012-03-30 Cezary Kaliszyk More on Aux
2012-03-30 Cezary Kaliszyk Close some of the obvious subgoals in Aux
2012-03-30 Cezary Kaliszyk Correct Aux and proof sketch that it's same as alpha-equality, following Dan Synek's proof.
2012-03-29 Cezary Kaliszyk Induction for Aux
2012-03-29 Cezary Kaliszyk Change definition of Aux to include alpha-convertibility for non-closed terms.
2012-03-27 Cezary Kaliszyk Define 'aux'
less more (0) tip