equal
deleted
inserted
replaced
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 |