src/HOL/Quotient_Examples/FSet.thy
Fri, 19 Jun 2015 15:55:22 +0200 nipkow renamed multiset_of -> mset
Thu, 07 Aug 2014 12:17:41 +0200 blanchet no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
less more (0) -30 -10 -3 tip