Lines Matching defs:entry
40 val entry = ty_antiq( ==`:string # method`== );
228 THEN STRIP_ASSUME_TAC (SPEC ���p:^entry���
545 ���REDL_entry : ^entry -> ^entry -> bool���;
1228 (!(M:^entry).
1560 THEN EXISTS_TAC ���e1:^entry���
1564 EXISTS_TAC ���e2:^entry���
1735 EXISTS_TAC ���e3:^entry���
1740 THEN EXISTS_TAC ���(l,m4):^entry���
1769 EXISTS_TAC ���e4':^entry���
1984 THEN FIRST_ASSUM (ASSUME_TAC o SPEC ���e1:^entry���)
2136 EXT_TAC ���e1:^entry���
2138 THEN EXT_TAC ���e2:^entry���