Lines Matching refs:SPEC
914 (map (fn tm => MP_TAC (SPEC_ALL (SPEC tm ALPHA1_height_induct_LEMMA)))
933 THEN STRIP_ASSUME_TAC (SPEC x th)
1031 THEN POP_ASSUM (MP_TAC o SPEC ���y:var���)
1032 THEN POP_ASSUM (MP_TAC o SPEC ���v:var���)
1039 THEN POP_ASSUM (MP_TAC o SPEC ���y:var���)
1040 THEN POP_ASSUM (MP_TAC o SPEC ���v:var���)
1232 THEN DISCH_THEN (MP_TAC o SPEC ���FV_obj1 (SUB1 s x)���)
1234 THEN POP_ASSUM (MP_TAC o SPEC ���x:var���)
1374 THEN POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���FV_obj1 (SUB1 s x')���)
1376 [ POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���x':var���)
1390 DISCH_THEN (STRIP_ASSUME_TAC o SPEC ���FV_obj1 (SUB1 s x')���)
1392 [ POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���x':var���)
1778 [ STRIP_ASSUME_TAC (SPEC ���o1:obj1��� obj1_cases)
1796 STRIP_ASSUME_TAC (SPEC ���o1:obj1��� obj1_cases)
1808 STRIP_ASSUME_TAC (SPEC ���o1':obj1��� obj1_cases)
1821 STRIP_ASSUME_TAC (SPEC ���o1':obj1��� obj1_cases)
1835 STRIP_ASSUME_TAC (SPEC ���d1':^dict1��� dict1_cases)
1848 STRIP_ASSUME_TAC (SPEC ���d1:^dict1��� dict1_cases)
1856 STRIP_ASSUME_TAC (SPEC ���e1:^entry1��� entry1_cases)
1865 STRIP_ASSUME_TAC (SPEC ���m1:method1��� method1_cases)
1959 THEN DISCH_THEN (ASSUME_TAC o SPEC ���OVAR1 y���)
1960 THEN DISCH_THEN (MP_TAC o SPEC ���OVAR1 x���)