Lines Matching defs:alpha
401 val alpha = Type.alpha
408 [] => Term.inst [alpha |-> elty] n
409 | x::xs => mk_comb(mk_comb(Term.inst [alpha |-> elty] c, x),
467 (alpha --> (alpha --> bool) --> (alpha --> bool))
468 val cEMP_t = Term.prim_new_const{Thy = "min", Name = "EMP"} (alpha --> bool)
494 val fx = mk_comb(mk_var("f", alpha --> bool), mk_var("x", alpha))
496 val bINS = Term.inst[alpha |-> bool] cINS_t
497 val bEMP = Term.inst[alpha |-> bool] cEMP_t
563 (mk_comb(cEMP_t, mk_var("x", alpha)))
734 alpha --> bool))