changeset 5235 | c404f25c58e8 |
parent 5212 | 2bc5b5cf0516 |
child 5290 | b755c7240348 |
--- 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); *)