lisp-runtime/implementation/lisp_opsScript.sml

156   val res2 = filter (not o can dest_sep_cond) res
158   val res3 = map dest_comb (filter (not o can dest_sep_hide) res2)
1096   val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR]
1099   val res2 = RW [GSYM lemma, STAR_ASSOC] res2
1103   val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA res1) res2
1166   val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR]
1169   val res2 = RW [GSYM lemma, STAR_ASSOC] res2
1173   val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA res1) res2
1360   val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2)
1361   val res = RW [STAR_ASSOC] (MATCH_MP (MATCH_MP fix_lemma res2) res1)
1407   val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2)
1408   val res = RW [STAR_ASSOC] (MATCH_MP (MATCH_MP fix_lemma res2) res1)
1499   val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR]
1513   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
1551   val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR]
1565   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
1626   val res2 = prove_spec th imp def pre_tm post_tm
1627   val res2 = RW [GSYM zLISP_raw] res2
1628   val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_FULL_GC]
1642   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
2476   val res2 = RW [GSYM zLISP_raw] result2
2477   val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_ERROR]
2491   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
2551   val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR]
2566   val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2)
2703   val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR]
2706   val res2 = RW [GSYM lemma, STAR_ASSOC] res2
2710   val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA2 res1) res2
2926   val res2 = prove_spec th imp def pre_tm post_tm
2930   val res2 = RW [lemma] res2
2932   val res = prove(goal,Cases_on `sf` THEN SIMP_TAC std_ss [res1,res2])
2965   val res2 = prove_spec th imp def pre_tm post_tm
2969   val res2 = PURE_REWRITE_RULE [lemma] res2
2970   val goal = subst [``T``|->``sf:bool``] (concl res2)
2972                        THEN ASSUME_TAC res1 THEN ASSUME_TAC res2
3006   val res2 = prove_spec th imp def pre_tm post_tm
3010   val res2 = RW [lemma] res2
3012   val res = prove(goal,Cases_on `cf` THEN SIMP_TAC std_ss [res1,res2])