src/HOL/Fun_Def.thy
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain