diff -r 701fa0ed77b7 -r c404f25c58e8 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Mon Aug 03 10:37:34 1998 +0200 +++ b/src/HOL/Tools/record_package.ML Tue Aug 04 09:21:44 1998 +0200 @@ -5,7 +5,7 @@ Extensible records with structural subtyping in HOL. TODO: - - field types: typedef; + - field types: datatype; - operations and theorems: split, split_all/ex, ...; - field constructor: more specific type for snd component (x_more etc. classes); *)