--- a/src/HOL/Set.thy Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Set.thy Thu Oct 30 22:45:19 2014 +0100
@@ -71,10 +71,11 @@
simproc_setup defined_Collect ("{x. P x & Q x}") = {*
fn _ => Quantifier1.rearrange_Collect
(fn _ =>
- rtac @{thm Collect_cong} 1 THEN
- rtac @{thm iffI} 1 THEN
+ resolve_tac @{thms Collect_cong} 1 THEN
+ resolve_tac @{thms iffI} 1 THEN
ALLGOALS
- (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
+ (EVERY' [REPEAT_DETERM o eresolve_tac @{thms conjE},
+ DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
*}
lemmas CollectE = CollectD [elim_format]
@@ -382,7 +383,7 @@
setup {*
map_theory_claset (fn ctxt =>
- ctxt addbefore ("bspec", fn _ => dtac @{thm bspec} THEN' assume_tac))
+ ctxt addbefore ("bspec", fn _ => dresolve_tac @{thms bspec} THEN' assume_tac))
*}
ML {*