Lines Matching defs:DB
18 structure DB :> DB =
23 val ERR = mk_HOL_ERR "DB";
71 datatype dbmap = DB of { namemap : (string, submap) Map.dict,
76 fun namemap (DB{namemap,...}) = namemap
77 fun revmap (DB{revmap,...}) = revmap
78 fun localmap (DB{localmap,...}) = localmap
79 fun updnamemap f (DB{namemap,revmap,localmap}) =
80 DB {namemap = f namemap, revmap = revmap, localmap = localmap}
81 fun updrevmap f (DB{namemap,revmap,localmap}) =
82 DB {namemap = namemap, revmap = f revmap, localmap=localmap}
83 fun updlocalmap f (DB{namemap,revmap,localmap}) =
84 DB {namemap = namemap, revmap = revmap, localmap = f localmap}
86 val empty_dbmap = DB {namemap = Map.mkDict String.compare,
182 val _ = Theory.register_hook("DB", hook)
218 val DB{namemap,...} = CT()
237 val DB{namemap,...} = CT()