Quot/Nominal/Abs.thy
Mon, 01 Feb 2010 18:57:20 +0100 Christian Urban added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case
less more (0) -1 tip