Lines Matching defs:typ
18 val typ = "{Thy: string, T: string list, C: string list, N: int list}"
33 PP.add_string typ]),
235 val typ = Type.--> (Term.type_of tm, Ty ty)
236 val vc = mk_local_const (f, typ)
238 Term.mk_var (f, typ) (* for recursion *)
247 val typ = Ty ty
249 mk_local_const (c, typ)
251 Term.mk_var (c, typ) (* for recursion *)
408 val typ = Type.--> (Type.--> (fty, fty), Type.--> (rty, rty))
417 | _ => mk_local_const (name, typ)
446 val typ = Ty ty
448 if typ = bitstringSyntax.bitstring_ty
450 else wordsSyntax.mk_word_extract (h, l, x, wordsSyntax.dest_word_type typ)