Lines Matching defs:alpha
36 (* the input term, not just alpha-equivalent. [TFM 90.07.11] *)
613 local val alpha = Type.alpha
625 (INST_TYPE [alpha |-> type_of Bvar] thm0)
1354 val th = INST_TYPE [Type.alpha |-> type_of lhs] EQ_SYM_EQ
1444 local val f = mk_var{Name="f",Ty=alpha-->bool}
1612 val def = INST_TYPE [alpha |-> type_of Bvar] EXISTS_UNIQUE_DEF
1637 (* --------------------------- COND_CONV "b => u | v" (u =alpha v) *)
1643 local val vt = genvar alpha
1644 and vf = genvar alpha
1650 val INST_TYPE' = INST_TYPE [alpha |-> type_of larm]
1681 val P = mk_var{Name="P", Ty=alpha-->bool}
1692 MP (SPEC Rand (INST_TYPE [alpha |-> type_of Bvar]