Lines Matching refs:SPEC
78 val th = SPEC f (MATCH_MP SPEC_FRAME th)
82 val th = SPEC x (MATCH_MP SPEC_FRAME th)
83 val th = SPEC post_tm (MATCH_MP SPEC_WEAKEN th)
125 val th = SPEC (mk_cond_star(pre_tm,pre)) th
301 val th = RW [Q.SPEC `n2w n` WORD_AND_COMM] th
471 val lisp_inv_0 = (DISCH_ALL o SIMP_RULE std_ss [] o Q.SPEC `0` o UNDISCH) lisp_inv_Val
472 val lisp_inv_1 = (DISCH_ALL o SIMP_RULE std_ss [] o Q.SPEC `1` o UNDISCH) lisp_inv_Val
1071 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1073 val th = SPEC (mk_var("r5",``:word32``)) th
1086 val th = SPEC (mk_var("r5",``:word32``)) th
1097 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1099 val th = Q.SPEC `edx` th
1112 val th = SPEC (mk_var("r5",``:word32``)) th
1125 val th = SPEC (mk_var("r5",``:word32``)) th
1136 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1138 val th = Q.SPEC `edx` th
1151 val th = SPEC (mk_var("r5",``:word32``)) th
1164 val th = SPEC (mk_var("r5",``:word32``)) th
1175 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1177 val th = Q.SPEC `edx` th
1368 val lisp_inv_test_zero = (SIMP_RULE std_ss [] o Q.SPEC `0`) lisp_inv_eq_0