Lines Matching defs:typ
18 val typ = "{Thy: string, T: string list, C: string list, N: int list}"
33 PP.add_string typ]),
233 val typ = Type.--> (Term.type_of tm, Ty ty)
234 val vc = mk_local_const (f, typ)
236 Term.mk_var (f, typ) (* for recursion *)
245 val typ = Ty ty
247 mk_local_const (c, typ)
249 Term.mk_var (c, typ) (* for recursion *)
405 val typ = Type.--> (Type.--> (fty, fty), Type.--> (rty, rty))
414 | _ => mk_local_const (name, typ)
443 val typ = Ty ty
445 if typ = bitstringSyntax.bitstring_ty
447 else wordsSyntax.mk_word_extract (h, l, x, wordsSyntax.dest_word_type typ)