hol88/mos-count/tempabs.ml

54 	PURE_REWRITE_TAC [Next;SYM (SPEC "t" ADD1)] THEN
67 	PURE_REWRITE_TAC [Next;SYM (SPEC "t" ADD1)] THEN
84 	DISJ_CASES_TAC (SPEC "t2 = t3" EXCLUDED_MIDDLE) THENL
86 	 DISJ_CASES_TAC (SPEC "t2 < t3" EXCLUDED_MIDDLE) THENL
90 let th1 = SPEC "t" (PURE_REWRITE_RULE [Inf] (ASSUME "Inf g"));;
110 let th3 = SPEC "t" (PURE_REWRITE_RULE [Inf] (ASSUME "Inf g"));;
143 	    (SELECT_RULE (SPEC "n" (ASSUME "!n. ?t. IsTimeOf n g t")))));;
150 	DISJ_CASES_TAC (SPEC "n" num_CASES) THENL
154 	     (SPEC "0" (ASSUME "!n. IsTimeOf n g (TimeOf g n)")));
161 	     (SPEC "SUC n'" (ASSUME "!n. IsTimeOf n g (TimeOf g n)")))]);;
201 	  (SPEC "SUC n" (UNDISCH (SPEC "g" TimeOf_DEFINED)));;
206 let th6 = SPEC "n" (UNDISCH (SPEC "g" TimeOf_DEFINED));;
221 	  (SPEC "SUC n" (UNDISCH (SPEC "g" TimeOf_DEFINED)));;
226 let th6 = SPEC "n" (UNDISCH (SPEC "g" TimeOf_DEFINED));;