Lines Matching refs:var
64 val _ = Hol_datatype `var = VAR of string => num`;
97 (* RW_TAC std_ss (type_rws "var") (* or list_ss or arith_ss *) *)
177 new_infix("is_variant", ==`:var->var->bool`==, 450);
470 ���SUC(CARD (s:var -> bool))���] LESS_CASES)
541 THEN ASSUME_TAC (INST_TYPE[==`:'a`== |-> ==`:var`==] FINITE_EMPTY)
584 THEN EXISTS_TAC ���s:var -> bool���
687 THEN IMP_RES_THEN (ASSUME_TAC o SPEC ���x:var���) variant_THM
745 THEN EXISTS_TAC ���(y:var) INSERT s���
849 THEN (MP_TAC o SPECL[���x:(var)list���,���(s:(var)-> bool) UNION t���])