Nominal/nominal_dt_alpha.ML
2010-09-20 Christian Urban introduced a general procedure for structural inductions; simplified reflexivity proof
2010-09-12 Christian Urban tuned code
2010-09-10 Christian Urban tuned (to conform with indentation policy of Markus)
less more (0) -30 -10 -3 tip