src/HOL/Relation.thy

   by (simp add: Id_on_def) 
 
 lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
   by (simp add: Id_on_def)
 
-lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
+lemma Id_onI [intro!]: "a : A ==> (a, a) : Id_on A"
   by (rule Id_on_eqI) (rule refl)
 
 lemma Id_onE [elim!]:
   "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   -- {* The general elimination rule. *}

 
 definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "``" 90)
 where
   "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
 
-declare Image_def [no_atp]
-
 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   by (simp add: Image_def)
 
 lemma Image_singleton: "r``{a} = {b. (a, b) : r}"
   by (simp add: Image_def)
 
 lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   by (rule Image_iff [THEN trans]) simp
 
-lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
+lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
   by (unfold Image_def) blast
 
 lemma ImageE [elim!]:
   "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
   by (unfold Image_def) (iprover elim!: CollectE bexE)