src/HOL/Tools/Function/pattern_split.ML
Wed, 27 Apr 2011 10:49:39 +0200 wenzelm eliminated obsolete Function_Lib.frees_in_term;
less more (0) -10 -1 tip