src/HOL/MicroJava/Comp/CorrCompTp.thy
Thu, 07 Aug 2014 12:17:41 +0200 blanchet no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
less more (0) -30 -10 -1 tip