src/FOLP/IFOLP.thy

 (** Congruence rules for predicate letters **)
 
 schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
   apply (rule iffI)
    apply (tactic {*
-     DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
+     DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
   done
 
 schematic_lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
   apply (rule iffI)
    apply (tactic {*
-     DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
+     DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
   done
 
 schematic_lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
   apply (rule iffI)
    apply (tactic {*
-     DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
+     DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *})
   done
 
 lemmas pred_congs = pred1_cong pred2_cong pred3_cong
 
 (*special case for the equality predicate!*)

 
 schematic_lemma disj_impE:
   assumes major: "p:(P|Q)-->S"
     and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
   shows "?p:R"
-  apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
+  apply (tactic {* DEPTH_SOLVE (assume_tac @{context} 1 ORELSE
       resolve_tac @{context} [@{thm disjI1}, @{thm disjI2}, @{thm impI},
         @{thm major} RS @{thm mp}, @{thm minor}] 1) *})
   done
 
 (*Simplifies the implication.  Classical version is stronger.