Lines Matching defs:alpha
554 val alpha = Type.alpha
561 [] => Term.inst [alpha |-> elty] n
562 | x::xs => mk_comb(mk_comb(Term.inst [alpha |-> elty] c, x),
620 (alpha --> (alpha --> bool) --> (alpha --> bool))
621 val cEMP_t = Term.prim_new_const{Thy = "min", Name = "EMP"} (alpha --> bool)
647 val fx = mk_comb(mk_var("f", alpha --> bool), mk_var("x", alpha))
649 val bINS = Term.inst[alpha |-> bool] cINS_t
650 val bEMP = Term.inst[alpha |-> bool] cEMP_t
716 (mk_comb(cEMP_t, mk_var("x", alpha)))
864 ty = alpha --> bool, print = true}