src/Provers/blast.ML
changeset 14466 b737e523fc6c
parent 13550 5a176b8dda84
child 14913 e993eabc7197
equal deleted inserted replaced
14465:8cc21ed7ef41 14466:b737e523fc6c
  1286 fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;
  1286 fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;
  1287 
  1287 
  1288 fun blast_tac cs i st = 
  1288 fun blast_tac cs i st = 
  1289     ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i 
  1289     ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i 
  1290      THEN flexflex_tac) st
  1290      THEN flexflex_tac) st
  1291     handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
  1291     handle TRANS s =>
       
  1292       ((if !trace then warning ("blast: " ^ s) else ()); 
       
  1293        Seq.empty);
  1292 
  1294 
  1293 fun Blast_tac i = blast_tac (Data.claset()) i;
  1295 fun Blast_tac i = blast_tac (Data.claset()) i;
  1294 
  1296 
  1295 
  1297 
  1296 (*** For debugging: these apply the prover to a subgoal and return 
  1298 (*** For debugging: these apply the prover to a subgoal and return