equal
deleted
inserted
replaced
78 | Bound of int |
78 | Bound of int |
79 | Abs of string*term |
79 | Abs of string*term |
80 | $ of term*term; |
80 | $ of term*term; |
81 type branch |
81 type branch |
82 val depth_tac : claset -> int -> int -> tactic |
82 val depth_tac : claset -> int -> int -> tactic |
|
83 val depth_limit : int ref |
83 val blast_tac : claset -> int -> tactic |
84 val blast_tac : claset -> int -> tactic |
84 val Blast_tac : int -> tactic |
85 val Blast_tac : int -> tactic |
85 val setup : (theory -> theory) list |
86 val setup : (theory -> theory) list |
86 (*debugging tools*) |
87 (*debugging tools*) |
87 val stats : bool ref |
88 val stats : bool ref |
1281 handle PROVE => Seq.empty); |
1282 handle PROVE => Seq.empty); |
1282 |
1283 |
1283 (*Public version with fixed depth*) |
1284 (*Public version with fixed depth*) |
1284 fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st; |
1285 fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st; |
1285 |
1286 |
|
1287 val depth_limit = ref 20; |
|
1288 |
1286 fun blast_tac cs i st = |
1289 fun blast_tac cs i st = |
1287 ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i |
1290 ((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i |
1288 THEN flexflex_tac) st |
1291 THEN flexflex_tac) st |
1289 handle TRANS s => |
1292 handle TRANS s => |
1290 ((if !trace then warning ("blast: " ^ s) else ()); |
1293 ((if !trace then warning ("blast: " ^ s) else ()); |
1291 Seq.empty); |
1294 Seq.empty); |
1292 |
1295 |