--- a/src/Pure/tactic.ML Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/tactic.ML Tue Oct 16 17:47:23 2012 +0200
@@ -53,6 +53,7 @@
val rename_tac: string list -> int -> tactic
val rotate_tac: int -> int -> tactic
val defer_tac: int -> tactic
+ val prefer_tac: int -> tactic
val filter_prems_tac: (term -> bool) -> int -> tactic
end;
@@ -318,6 +319,9 @@
(*Rotates the given subgoal to be the last.*)
fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
+(*Rotates the given subgoal to be the first.*)
+fun prefer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1);
+
(* remove premises that do not satisfy p; fails if all prems satisfy p *)
fun filter_prems_tac p =
let fun Then NONE tac = SOME tac