Lines Matching defs:typ
1908 val typ = fcpSyntax.mk_int_numeric_type sz
1909 val sz_thm = SIZES_CONV (wordsSyntax.mk_dimword typ)
1916 (Thm.INST_TYPE [Type.alpha |-> typ] intro_thm))
2594 val typ = type_of (rand tm)
2596 (typ = num) orelse is_word_type typ
2630 val typ = fcpLib.index_type N
2631 val TYPE = mk_type ("cart", [bool, typ])
2639 Thm.INST_TYPE [``:'a`` |-> typ]) INT_MIN_def)
2642 Thm.INST_TYPE [``:'a`` |-> typ]) dimword_IS_TWICE_INT_MIN)