src/HOL/Nominal/Examples/Class.thy
Thu, 21 Jun 2007 22:10:16 +0200 wenzelm tuned proofs -- avoid implicit prems;
less more (0) -10 -1 tip