Lines Matching defs:alpha
40 * the input term, not just alpha-equivalent. [TFM 90.07.11] *
666 val alpha = Type.alpha
679 (INST_TYPE [alpha |-> type_of Bvar] thm0)
1533 val th = INST_TYPE [Type.alpha |-> type_of lhs] EQ_SYM_EQ
1641 val f = mk_var {Name = "f", Ty = alpha --> bool}
2249 val def = INST_TYPE [alpha |-> type_of Bvar] EXISTS_UNIQUE_DEF
2274 * --------------------------- COND_CONV "b => u | v" (u =alpha v) *
2281 val vt = genvar alpha
2282 and vf = genvar alpha
2289 val INST_TYPE' = INST_TYPE [alpha |-> type_of larm]
2314 val P = mk_var {Name = "P", Ty = alpha-->bool}
2326 (INST_TYPE [alpha |-> type_of Bvar] (GEN P (DISCH ex1P th2))))