equal
deleted
inserted
replaced
17 val all_tac : tactic |
17 val all_tac : tactic |
18 val ALLGOALS : (int -> tactic) -> tactic |
18 val ALLGOALS : (int -> tactic) -> tactic |
19 val APPEND : tactic * tactic -> tactic |
19 val APPEND : tactic * tactic -> tactic |
20 val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
20 val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
21 val CHANGED : tactic -> tactic |
21 val CHANGED : tactic -> tactic |
|
22 val CHANGED_GOAL : (int -> tactic) -> int -> tactic |
22 val COND : (thm -> bool) -> tactic -> tactic -> tactic |
23 val COND : (thm -> bool) -> tactic -> tactic -> tactic |
23 val DETERM : tactic -> tactic |
24 val DETERM : tactic -> tactic |
24 val EVERY : tactic list -> tactic |
25 val EVERY : tactic list -> tactic |
25 val EVERY' : ('a -> tactic) list -> 'a -> tactic |
26 val EVERY' : ('a -> tactic) list -> 'a -> tactic |
26 val EVERY1 : (int -> tactic) list -> tactic |
27 val EVERY1 : (int -> tactic) list -> tactic |
55 val THEN : tactic * tactic -> tactic |
56 val THEN : tactic * tactic -> tactic |
56 val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
57 val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
57 val THEN_ALL_NEW : (int -> tactic) * (int -> tactic) -> int -> tactic |
58 val THEN_ALL_NEW : (int -> tactic) * (int -> tactic) -> int -> tactic |
58 val THEN_ELSE : tactic * (tactic*tactic) -> tactic |
59 val THEN_ELSE : tactic * (tactic*tactic) -> tactic |
59 val traced_tac : (thm -> (thm * thm Seq.seq) option) -> tactic |
60 val traced_tac : (thm -> (thm * thm Seq.seq) option) -> tactic |
60 val tracify : bool ref -> tactic -> thm -> thm Seq.seq |
61 val tracify : bool ref -> tactic -> tactic |
61 val trace_REPEAT : bool ref |
62 val trace_REPEAT : bool ref |
62 val TRY : tactic -> tactic |
63 val TRY : tactic -> tactic |
63 val TRYALL : (int -> tactic) -> tactic |
64 val TRYALL : (int -> tactic) -> tactic |
64 end; |
65 end; |
65 |
66 |
320 |
321 |
321 |
322 |
322 (*Make a tactic for subgoal i, if there is one. *) |
323 (*Make a tactic for subgoal i, if there is one. *) |
323 fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1), i) st |
324 fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1), i) st |
324 handle Subscript => Seq.empty; |
325 handle Subscript => Seq.empty; |
|
326 |
|
327 (*Returns all states that have changed in subgoal i, counted from the LAST |
|
328 subgoal. For stac, for example.*) |
|
329 fun CHANGED_GOAL tac i st = |
|
330 let val j = nprems_of st - i |
|
331 val t = List.nth(prems_of st, i-1) |
|
332 fun diff st' = |
|
333 not (nprems_of st' > j (*subgoal is still there*) |
|
334 andalso |
|
335 t aconv List.nth(prems_of st', nprems_of st' - j - 1)) |
|
336 in Seq.filter diff (tac i st) end |
|
337 handle Subscript => Seq.empty (*no subgoal i*); |
325 |
338 |
326 fun ALLGOALS_RANGE tac (i:int) j st = |
339 fun ALLGOALS_RANGE tac (i:int) j st = |
327 if i > j then all_tac st |
340 if i > j then all_tac st |
328 else (tac j THEN ALLGOALS_RANGE tac i (j - 1)) st; |
341 else (tac j THEN ALLGOALS_RANGE tac i (j - 1)) st; |
329 |
342 |