src/HOL/FunDef.thy
Mon, 25 Jun 2007 12:16:27 +0200 krauss removed "sum_tools.ML" in favour of BalancedTree
less more (0) -10 -1 tip