src/FOLP/FOLP.thy

   assumes major: "p:P-->Q"
     and r1: "!!x. x:~P ==> f(x):R"
     and r2: "!!y. y:Q ==> g(y):R"
   shows "?p : R"
   apply (rule excluded_middle [THEN disjE])
-   apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
+   apply (tactic {* DEPTH_SOLVE (assume_tac @{context} 1 ORELSE
        resolve_tac @{context} [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *})
   done
 
 (*Double negation law*)
 schematic_lemma notnotD: "p:~~P ==> ?p : P"

     and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
   shows "?p : R"
   apply (insert major)
   apply (unfold iff_def)
   apply (rule conjE)
-  apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE
-      eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE
+  apply (tactic {* DEPTH_SOLVE_1 (eresolve_tac @{context} @{thms impCE} 1 ORELSE
+      eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN assume_tac @{context} 1 ORELSE
+      assume_tac @{context} 1 ORELSE
       resolve_tac @{context} [@{thm r1}, @{thm r2}] 1) *})+
   done
 
 
 (*Should be used as swap since ~P becomes redundant*)

 (
   val sizef = size_of_thm
   val mp = @{thm mp}
   val not_elim = @{thm notE}
   val swap = @{thm swap}
-  val hyp_subst_tacs = [hyp_subst_tac]
+  fun hyp_subst_tacs ctxt = [hyp_subst_tac ctxt]
 );
 open Cla;
 
 (*Propositional rules
   -- iffCE might seem better, but in the examples in ex/cla