TFL/post.ML
changeset 13501 79242cccaddc
parent 12488 83acab8042ad
child 14240 d3843feb9de7
equal deleted inserted replaced
13500:2222c7a0e8bb 13501:79242cccaddc
    69  *--------------------------------------------------------------------------*)
    69  *--------------------------------------------------------------------------*)
    70 fun std_postprocessor strict cs ss wfs =
    70 fun std_postprocessor strict cs ss wfs =
    71   Prim.postprocess strict
    71   Prim.postprocess strict
    72    {wf_tac     = REPEAT (ares_tac wfs 1),
    72    {wf_tac     = REPEAT (ares_tac wfs 1),
    73     terminator = asm_simp_tac ss 1
    73     terminator = asm_simp_tac ss 1
    74                  THEN TRY (arith_tac 1 ORELSE
    74                  THEN TRY (silent_arith_tac 1 ORELSE
    75                            fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    75                            fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    76     simplifier = Rules.simpl_conv ss []};
    76     simplifier = Rules.simpl_conv ss []};
    77 
    77 
    78 
    78 
    79 
    79