src/HOL/MicroJava/Comp/LemmasComp.thy
Wed, 07 Feb 2007 17:44:07 +0100 berghofe Adapted to new inductive definition package.
less more (0) -1 tip