equal
deleted
inserted
replaced
1 (* Title: Pure/tactic.ML |
1 (* Title: Pure/tactic.ML |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
3 |
5 |
4 Fundamental tactics. |
6 Basic tactics. |
|
7 *) |
5 *) |
8 |
6 |
9 signature BASIC_TACTIC = |
7 signature BASIC_TACTIC = |
10 sig |
8 sig |
11 val trace_goalno_tac: (int -> tactic) -> int -> tactic |
9 val trace_goalno_tac: (int -> tactic) -> int -> tactic |
190 in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end; |
188 in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end; |
191 |
189 |
192 (*Determine print names of goal parameters (reversed)*) |
190 (*Determine print names of goal parameters (reversed)*) |
193 fun innermost_params i st = |
191 fun innermost_params i st = |
194 let val (_, _, Bi, _) = dest_state (st, i) |
192 let val (_, _, Bi, _) = dest_state (st, i) |
195 in rename_wrt_term Bi (Logic.strip_params Bi) end; |
193 in Term.rename_wrt_term Bi (Logic.strip_params Bi) end; |
196 |
194 |
197 (*params of subgoal i as they are printed*) |
195 (*params of subgoal i as they are printed*) |
198 fun params_of_state i st = rev (innermost_params i st); |
196 fun params_of_state i st = rev (innermost_params i st); |
199 |
197 |
200 (* |
198 (* |