src/HOL/MicroJava/Comp/CorrComp.thy
Mon, 11 Oct 2004 07:42:22 +0200 nipkow Proofs needed to be updated because induction now preserves name of
less more (0) -1 tip