src/Provers/blast.ML
changeset 36787 f60e4dd6d76f
parent 36001 992839c4be90
child 36960 01594f816e3a
equal deleted inserted replaced
36786:b7a62e7dec00 36787:f60e4dd6d76f
  1276 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
  1276 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
  1277 
  1277 
  1278 val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
  1278 val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
  1279 
  1279 
  1280 fun blast_tac cs i st =
  1280 fun blast_tac cs i st =
  1281     ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
  1281     ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
  1282         (timing_depth_tac (start_timing ()) cs) 0) i
  1282         (timing_depth_tac (start_timing ()) cs) 0) i
  1283      THEN flexflex_tac) st
  1283      THEN flexflex_tac) st
  1284     handle TRANS s =>
  1284     handle TRANS s =>
  1285       ((if !trace then warning ("blast: " ^ s) else ());
  1285       ((if !trace then warning ("blast: " ^ s) else ());
  1286        Seq.empty);
  1286        Seq.empty);