src/HOL/Tools/record_package.ML
changeset 5235 c404f25c58e8
parent 5212 2bc5b5cf0516
child 5290 b755c7240348
     1.1 --- a/src/HOL/Tools/record_package.ML	Mon Aug 03 10:37:34 1998 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Tue Aug 04 09:21:44 1998 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Extensible records with structural subtyping in HOL.
     1.5  
     1.6  TODO:
     1.7 -  - field types: typedef;
     1.8 +  - field types: datatype;
     1.9    - operations and theorems: split, split_all/ex, ...;
    1.10    - field constructor: more specific type for snd component (x_more etc. classes);
    1.11  *)