src/HOL/Relation.thy

   by (simp add: diag_def) 
 
 lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
   by (simp add: diag_def)
 
-lemma diagI [intro!]: "a : A ==> (a, a) : diag A"
+lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
   by (rule diag_eqI) (rule refl)
 
 lemma diagE [elim!]:
   "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   -- {* The general elimination rule. *}

   by (unfold sym_def) blast
 
 
 subsection {* Domain *}
 
+declare Domain_def [noatp]
+
 lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
   by (unfold Domain_def) blast
 
 lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
   by (iprover intro!: iffD2 [OF Domain_iff])

   done
 
 
 subsection {* Image of a set under a relation *}
 
+declare Image_def [noatp]
+
 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]: "(a, b) : r ==> a : A ==> b : r``A"
+lemma ImageI [intro,noatp]: "(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)