src/HOL/Tools/record.ML
Fri, 19 Jun 2009 17:23:21 +0200 discontinued ancient tradition to suffix certain ML module names with "_package"