src/Provers/blast.ML
changeset 23985 83e6e9ad0f4f
parent 23958 bb838771157f
child 24062 845c0d693328
equal deleted inserted replaced
23984:aaff3bc5ec28 23985:83e6e9ad0f4f
  1244 
  1244 
  1245 (*Tactic using tableau engine and proof reconstruction.
  1245 (*Tactic using tableau engine and proof reconstruction.
  1246  "start" is CPU time at start, for printing SEARCH time
  1246  "start" is CPU time at start, for printing SEARCH time
  1247         (also prints reconstruction time)
  1247         (also prints reconstruction time)
  1248  "lim" is depth limit.*)
  1248  "lim" is depth limit.*)
  1249 fun timing_depth_tac start cs lim i st0 = CRITICAL (fn () =>
  1249 fun timing_depth_tac start cs lim i st0 = NAMED_CRITICAL "blast" (fn () =>
  1250   let val st = (initialize (theory_of_thm st0); Conv.gconv_rule ObjectLogic.atomize_prems i st0);
  1250   let val st = (initialize (theory_of_thm st0); Conv.gconv_rule ObjectLogic.atomize_prems i st0);
  1251       val sign = Thm.theory_of_thm st
  1251       val sign = Thm.theory_of_thm st
  1252       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
  1252       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
  1253       val hyps  = strip_imp_prems skoprem
  1253       val hyps  = strip_imp_prems skoprem
  1254       and concl = strip_imp_concl skoprem
  1254       and concl = strip_imp_concl skoprem