src/HOL/Tools/Function/function_lib.ML
Sun, 16 Oct 2011 18:48:30 +0200 wenzelm added Term.dummy_pattern conveniences;
less more (0) -10 -1 tip