Lines Matching defs:entry
36 val entry = ty_antiq( ==`:string # method`== );
110 (!(M:^entry) N L x y.
350 (!e1:^entry. Re e1 e1) /\
360 (!e1 e2:^entry. Re e1 e2 ==> Re e2 e1) /\
368 (!e1 e2 e3:^entry. Re e1 e2 /\ Re e2 e3 ==> Re e1 e3) /\
401 ���RED1_entry : (obj -> obj -> bool) -> ^entry -> ^entry -> bool���;
872 ���RED_entry : (obj -> obj -> bool) -> ^entry -> ^entry -> bool���;
1098 THEN EXISTS_TAC ���CONS ((M:^entry) <[ [x,N']) (M' <[ [x,N])���
1137 ���REQUAL_entry : (obj -> obj -> bool) -> ^entry -> ^entry -> bool���;
1519 EXISTS_TAC ���e2:^entry���
1526 THEN EXISTS_TAC ���Z:^entry���
1538 THEN EXISTS_TAC ���d:^entry���
1583 EXISTS_TAC ���Z:^entry���,
1653 (!(M:^entry) (N:^entry) L x.