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;
less more (0) -10 -4 tip