Lines Matching defs:data
6 type data = LoadableThyData.t
45 destfn: takes polymorphic theory data and turns it into the
46 structured theorem data we want to use
48 the theory data. Doesn't perform any associated update in
55 type destfn = data -> (string * thm) list option
104 val (data, _) = mk' [s]
106 LoadableThyData.write_data_update {thydataty = ty, data = data}
161 data = #1 (mk (map #1 ok))})
172 val (data, namedthms) = mk [s]
175 write_data_update {thydataty = name, data = data}