Lines Matching defs:var
112 val (var, a) = dest_forall tm
116 if not(var = v)
119 SYM (RIGHT_CONV_RULE ((GEN_ALPHA_CONV var) THENC
121 (ISPECL [pred,mk_abs(var,t)] dthm))
134 val (var,pred,conj) = dest_res_forall tm
136 val left_pred = mk_abs(var,left)
137 val right_pred = mk_abs(var,right)
480 <varstruct> ::= <var> | (<varstruct>,...,<varstruct>)
502 <lhs> ::= <var> | <lhs> <varstruct>
521 else raise ERR "check_lhs" "var used twice"
558 raise ERR "RESQ_DEF_EXISTS_RULE" "restrict bound var not in lhs"
561 raise ERR "RESQ_DEF_EXISTS_RULE" "unbound var in rhs"