Lines Matching refs:SPEC
264 SPEC y (MATCH_MP INT_DIVIDES_RMUL ldel_divides)
276 SPEC y (MATCH_MP INT_DIVIDES_RMUL ldel_divides)
360 val delta_ok = CONJ zero_lt_delta (SPEC delta_tm INT_LE_REFL)
583 SYM (SPEC e elim_neg_ones)
646 val disj2_exm = SPEC disj2 EXCLUDED_MIDDLE
786 val e_eq_e11 = SYM (SPEC e elim_minus_ones)
960 val e_eq_11 = SYM (SPEC e elim_neg_ones)
1071 SPEC change_by_dmultiples with u, and MP with zero_lt_u to get
1074 val Fx0_less_ud = MP (SPEC u change_by_dmultiples) zero_lt_u
1075 (* SPEC choose_lemma with x0 - u * d and MP with x0_less_ud to get
1081 MP (SPEC x0_less_ud_tm choose_lemma) x0_less_ud