--- a/src/FOLP/IFOLP.thy Sat Jul 18 20:53:05 2015 +0200
+++ b/src/FOLP/IFOLP.thy Sat Jul 18 20:54:56 2015 +0200
@@ -504,19 +504,19 @@
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
@@ -543,7 +543,7 @@
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