src/HOL/Tools/Function/function_lib.ML
Sun, 16 Oct 2011 18:48:30 +0200 wenzelm added Term.dummy_pattern conveniences;
Wed, 27 Apr 2011 23:04:28 +0200 wenzelm merged
Wed, 27 Apr 2011 21:17:47 +0200 krauss inlined Function_Lib.replace_frees, which is used only once
Wed, 27 Apr 2011 21:50:04 +0200 wenzelm clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
Wed, 27 Apr 2011 10:49:39 +0200 wenzelm eliminated obsolete Function_Lib.frees_in_term;
Mon, 13 Dec 2010 10:15:27 +0100 krauss eliminated dest_all_all_ctx
Mon, 13 Dec 2010 10:15:26 +0100 krauss private term variant of Variable.focus
less more (0) -10 -7 tip