--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Jul 16 10:48:20 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Jul 16 12:23:22 2015 +0200
@@ -54,6 +54,11 @@
val rapp: term -> term -> term
+ val rtac: Proof.context -> thm -> int -> tactic
+ val etac: Proof.context -> thm -> int -> tactic
+ val dtac: Proof.context -> thm -> int -> tactic
+ val ftac: Proof.context -> thm -> int -> tactic
+
val list_all_free: term list -> term -> term
val list_exists_free: term list -> term -> term
@@ -273,4 +278,9 @@
fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
+fun rtac ctxt thm = resolve_tac ctxt [thm];
+fun etac ctxt thm = eresolve_tac ctxt [thm];
+fun dtac ctxt thm = dresolve_tac ctxt [thm];
+fun ftac ctxt thm = forward_tac ctxt [thm];
+
end;