Lines Matching defs:alpha
50 * the input term, not just alpha-equivalent. [TFM 90.07.11] *
674 val alpha = Type.alpha
687 (INST_TYPE [alpha |-> type_of Bvar] thm0)
1543 val th = INST_TYPE [Type.alpha |-> type_of lhs] EQ_SYM_EQ
1651 val f = mk_var {Name = "f", Ty = alpha --> bool}
2262 val def = INST_TYPE [alpha |-> type_of Bvar] EXISTS_UNIQUE_DEF
2287 * --------------------------- COND_CONV "b => u | v" (u =alpha v) *
2294 val vt = genvar alpha
2295 and vf = genvar alpha
2302 val INST_TYPE' = INST_TYPE [alpha |-> type_of larm]
2337 val P = mk_var {Name = "P", Ty = alpha-->bool}
2349 (INST_TYPE [alpha |-> type_of Bvar] (GEN P (DISCH ex1P th2))))