equal
deleted
inserted
replaced
338 val d = np-i (*distance from END*) |
338 val d = np-i (*distance from END*) |
339 val t = Thm.term_of (Thm.cprem_of st i) |
339 val t = Thm.term_of (Thm.cprem_of st i) |
340 fun diff st' = |
340 fun diff st' = |
341 Thm.nprems_of st' - d <= 0 (*the subgoal no longer exists*) |
341 Thm.nprems_of st' - d <= 0 (*the subgoal no longer exists*) |
342 orelse |
342 orelse |
343 not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d)))) |
343 not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d)))) |
344 in Seq.filter diff (tac i st) end |
344 in Seq.filter diff (tac i st) end |
345 handle General.Subscript => Seq.empty (*no subgoal i*); |
345 handle General.Subscript => Seq.empty (*no subgoal i*); |
346 |
346 |
347 (*Returns all states where some subgoals have been solved. For |
347 (*Returns all states where some subgoals have been solved. For |
348 subgoal-based tactics this means subgoal i has been solved |
348 subgoal-based tactics this means subgoal i has been solved |