src/HOL/Hoare/hoare_tac.ML

 (*****************************************************************************)
 
 fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
   before_set2pred_simp_tac ctxt i THEN_MAYBE
   EVERY [
-    rtac subsetI i,
-    rtac CollectI i,
-    dtac CollectD i,
+    resolve_tac ctxt [subsetI] i,
+    resolve_tac ctxt [CollectI] i,
+    dresolve_tac ctxt [CollectD] i,
     TRY (split_all_tac ctxt i) THEN_MAYBE
      (rename_tac var_names i THEN
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
 
 (*******************************************************************************)

 (** and transforms any other into predicates, applying then                   **)
 (** the tactic chosen by the user, which may solve the subgoal completely.    **)
 (*******************************************************************************)
 
 fun max_simp_tac ctxt var_names tac =
-  FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
+  FIRST' [resolve_tac ctxt [subset_refl],
+    set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
 
 fun basic_simp_tac ctxt var_names tac =
   simp_tac
     (put_simpset HOL_basic_ss ctxt
       addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])

 
 fun hoare_rule_tac ctxt (vars, Mlem) tac =
   let
     val var_names = map (fst o dest_Free) vars;
     fun wlp_tac i =
-      rtac @{thm SeqRule} i THEN rule_tac false (i + 1)
+      resolve_tac ctxt @{thms SeqRule} i THEN rule_tac false (i + 1)
     and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
       ((wlp_tac i THEN rule_tac pre_cond i)
         ORELSE
         (FIRST [
-          rtac @{thm SkipRule} i,
-          rtac @{thm AbortRule} i,
+          resolve_tac ctxt @{thms SkipRule} i,
+          resolve_tac ctxt @{thms AbortRule} i,
           EVERY [
-            rtac @{thm BasicRule} i,
-            rtac Mlem i,
+            resolve_tac ctxt @{thms BasicRule} i,
+            resolve_tac ctxt [Mlem] i,
             split_simp_tac ctxt i],
           EVERY [
-            rtac @{thm CondRule} i,
+            resolve_tac ctxt @{thms CondRule} i,
             rule_tac false (i + 2),
             rule_tac false (i + 1)],
           EVERY [
-            rtac @{thm WhileRule} i,
+            resolve_tac ctxt @{thms WhileRule} i,
             basic_simp_tac ctxt var_names tac (i + 2),
             rule_tac true (i + 1)]]
-         THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i)));
+         THEN (
+           if pre_cond then basic_simp_tac ctxt var_names tac i
+           else resolve_tac ctxt [subset_refl] i)));
   in rule_tac end;
 
 
 (** tac is the tactic the user chooses to solve or simplify **)
 (** the final verification conditions                       **)