src/HOL/Quotient_Examples/FSet.thy
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'
Wed, 19 Feb 2014 16:32:37 +0100 blanchet merged 'List.set' with BNF-generated 'set'
Mon, 14 Oct 2013 15:01:41 +0200 kuncar declare Quotient_Examples/FSet.thy as almost obsolete
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Fri, 08 Mar 2013 09:34:38 +0100 traytel some simp rules for fset
Fri, 13 Apr 2012 14:00:26 +0200 wenzelm updated headers;
less more (0) -30 -10 -7 tip