equal
deleted
inserted
replaced
1256 else (); |
1256 else (); |
1257 Seq.make(fn()=> cell)) |
1257 Seq.make(fn()=> cell)) |
1258 end |
1258 end |
1259 in |
1259 in |
1260 prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) |
1260 prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) |
1261 |> Seq.maps Thm.flexflex_rule |
|
1262 end |
1261 end |
1263 handle PROVE => Seq.empty |
1262 handle PROVE => Seq.empty |
1264 | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty); |
1263 | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty); |
1265 |
1264 |
1266 fun depth_tac ctxt lim i st = |
1265 fun depth_tac ctxt lim i st = |