src/HOL/Fun.thy

 lemma inj_on_swap_iff [simp]:
   assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
 proof 
   assume "inj_on (swap a b f) A"
   with A have "inj_on (swap a b (swap a b f)) A" 
-    by (rules intro: inj_on_imp_inj_on_swap) 
+    by (iprover intro: inj_on_imp_inj_on_swap) 
   thus "inj_on f A" by simp 
 next
   assume "inj_on f A"
-  with A show "inj_on (swap a b f) A" by (rules intro: inj_on_imp_inj_on_swap)
+  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
 qed
 
 lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
 apply (simp add: surj_def swap_def, clarify)
 apply (rule_tac P = "y = f b" in case_split_thm, blast)