src/HOL/Relation.thy
changeset 54147 97a8ff4e4ac9
parent 53680 c5096c22892b
child 54410 0a578fb7fb73
     1.1 --- a/src/HOL/Relation.thy	Fri Oct 18 10:35:57 2013 +0200
     1.2 +++ b/src/HOL/Relation.thy	Fri Oct 18 10:43:20 2013 +0200
     1.3 @@ -478,7 +478,7 @@
     1.4  lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
     1.5    by (simp add: Id_on_def)
     1.6  
     1.7 -lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
     1.8 +lemma Id_onI [intro!]: "a : A ==> (a, a) : Id_on A"
     1.9    by (rule Id_on_eqI) (rule refl)
    1.10  
    1.11  lemma Id_onE [elim!]:
    1.12 @@ -939,8 +939,6 @@
    1.13  where
    1.14    "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
    1.15  
    1.16 -declare Image_def [no_atp]
    1.17 -
    1.18  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
    1.19    by (simp add: Image_def)
    1.20  
    1.21 @@ -950,7 +948,7 @@
    1.22  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
    1.23    by (rule Image_iff [THEN trans]) simp
    1.24  
    1.25 -lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
    1.26 +lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
    1.27    by (unfold Image_def) blast
    1.28  
    1.29  lemma ImageE [elim!]: