equal
deleted
inserted
replaced
40 |
40 |
41 (** datatypes **) |
41 (** datatypes **) |
42 |
42 |
43 (* data kind 'datatypes' *) |
43 (* data kind 'datatypes' *) |
44 |
44 |
45 val datatypesK = "datatypes"; |
45 val datatypesK = "HOL/datatypes"; |
46 exception DatatypeInfo of datatype_info Symtab.table; |
46 exception DatatypeInfo of datatype_info Symtab.table; |
47 |
47 |
48 local |
48 local |
49 val empty = DatatypeInfo Symtab.empty; |
49 val empty = DatatypeInfo Symtab.empty; |
50 |
50 |
77 |
77 |
78 (** records **) |
78 (** records **) |
79 |
79 |
80 (* data kind 'records' *) |
80 (* data kind 'records' *) |
81 |
81 |
82 val recordsK = "records"; |
82 val recordsK = "HOL/records"; |
83 exception Records of record_info Symtab.table; |
83 exception Records of record_info Symtab.table; |
84 |
84 |
85 |
85 |
86 (* methods *) |
86 (* methods *) |
87 |
87 |