TFL/post.ML
changeset 12488 83acab8042ad
parent 12341 08afd1003151
child 13501 79242cccaddc
equal deleted inserted replaced
12487:bbd564190c9b 12488:83acab8042ad
    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 (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    74                  THEN TRY (arith_tac 1 ORELSE
       
    75                            fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
    75     simplifier = Rules.simpl_conv ss []};
    76     simplifier = Rules.simpl_conv ss []};
    76 
    77 
    77 
    78 
    78 
    79 
    79 val concl = #2 o Rules.dest_thm;
    80 val concl = #2 o Rules.dest_thm;