src/HOL/Fun_Def_Base.thy
Mon, 20 Jan 2014 21:32:41 +0100 blanchet moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
less more (0) tip