src/HOL/Nominal/Examples/SOS.thy
Thu, 31 May 2007 14:47:20 +0200 urbanc introduced symmetric variants of the lemmas for alpha-equivalence
less more (0) -10 -1 tip