Quot/Nominal/LFex.thy
Tue, 02 Feb 2010 10:43:48 +0100 Cezary Kaliszyk With induct instead of induct_tac, just one induction is sufficient.
less more (0) -1 tip