src/HOL/Tools/Function/function_lib.ML
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 -2 tip