lisp-runtime/implementation/lisp_opsScript.sml

155   val res2 = filter (not o can dest_sep_cond) res
157   val res3 = map dest_comb (filter (not o can dest_sep_hide) res2)
1093   val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR]
1096   val res2 = RW [GSYM lemma, STAR_ASSOC] res2
1100   val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA res1) res2
1163   val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR]
1166   val res2 = RW [GSYM lemma, STAR_ASSOC] res2
1170   val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA res1) res2
1357   val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2)
1358   val res = RW [STAR_ASSOC] (MATCH_MP (MATCH_MP fix_lemma res2) res1)
1404   val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2)
1405   val res = RW [STAR_ASSOC] (MATCH_MP (MATCH_MP fix_lemma res2) res1)
1496   val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR]
1510   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
1548   val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR]
1562   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
1623   val res2 = prove_spec th imp def pre_tm post_tm
1624   val res2 = RW [GSYM zLISP_raw] res2
1625   val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_FULL_GC]
1639   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
2473   val res2 = RW [GSYM zLISP_raw] result2
2474   val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_ERROR]
2488   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
2548   val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR]
2563   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
2700   val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR]
2703   val res2 = RW [GSYM lemma, STAR_ASSOC] res2
2707   val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA2 res1) res2
2923   val res2 = prove_spec th imp def pre_tm post_tm
2927   val res2 = RW [lemma] res2
2929   val res = prove(goal,Cases_on `sf` THEN SIMP_TAC std_ss [res1,res2])
2962   val res2 = prove_spec th imp def pre_tm post_tm
2966   val res2 = PURE_REWRITE_RULE [lemma] res2
2967   val goal = subst [``T``|->``sf:bool``] (concl res2)
2969                        THEN ASSUME_TAC res1 THEN ASSUME_TAC res2
3003   val res2 = prove_spec th imp def pre_tm post_tm
3007   val res2 = RW [lemma] res2
3009   val res = prove(goal,Cases_on `cf` THEN SIMP_TAC std_ss [res1,res2])