src/HOL/Tools/Function/partial_function.ML
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
less more (0) -30 -10 -1 tip