src/HOL/Tools/function_package/sum_tree.ML
Sat, 27 Dec 2008 17:49:15 +0100 krauss removed duplicate sum_case used only by function package;
Thu, 06 Dec 2007 12:23:52 +0100 krauss factored out handling of sum types again
less more (0) tip