TFL/post.sml
changeset 3572 5ec1589eac1b
parent 3556 229a40c2b19e
child 3927 27c63b757af5
equal deleted inserted replaced
3571:f1c8fa0f0bf9 3572:5ec1589eac1b
   152                U.itlist (fn th => fn (So,Si,St) =>
   152                U.itlist (fn th => fn (So,Si,St) =>
   153                      if (id_thm th) then (So, Si, th::St) else
   153                      if (id_thm th) then (So, Si, th::St) else
   154                      if (solved th) then (th::So, Si, St) 
   154                      if (solved th) then (th::So, Si, St) 
   155                      else (So, th::Si, St)) nested_tcs ([],[],[])
   155                      else (So, th::Si, St)) nested_tcs ([],[],[])
   156               val simplified' = map join_assums simplified
   156               val simplified' = map join_assums simplified
   157               val rewr = rewrite (solved @ simplified' @
   157               val rewr = full_simplify (ss addsimps (solved @ simplified'));
   158                 #simps (Thm.dest_mss (#mss (rep_ss ss))));
       
   159               val induction' = rewr induction
   158               val induction' = rewr induction
   160               and rules'     = rewr rules
   159               and rules'     = rewr rules
   161               val dummy = writeln "Postprocessing done."
   160               val dummy = writeln "Postprocessing done."
   162           in
   161           in
   163           {induction = induction',
   162           {induction = induction',