author | paulson |
Thu, 05 Sep 1996 18:29:43 +0200 | |
changeset 1955 | 5309416236b6 |
parent 1954 | 4b5b2d04782c |
child 1956 | 589af052bcd4 |
--- a/src/Pure/tactic.ML Thu Sep 05 18:28:54 1996 +0200 +++ b/src/Pure/tactic.ML Thu Sep 05 18:29:43 1996 +0200 @@ -77,6 +77,7 @@ val subgoal_tac: string -> int -> tactic val subgoals_tac: string list -> int -> tactic val subgoals_of_brl: bool * thm -> int + val thin_tac: string -> int -> tactic val trace_goalno_tac: (int -> tactic) -> int -> tactic end;