src/HOL/Relation.thy
changeset 35828 46cfc4b8112e
parent 33218 ecb5cd453ef2
child 36728 ae397b810c8b
     1.1 --- a/src/HOL/Relation.thy	Wed Mar 17 19:37:44 2010 +0100
     1.2 +++ b/src/HOL/Relation.thy	Thu Mar 18 12:58:52 2010 +0100
     1.3 @@ -121,7 +121,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!,noatp]: "a : A ==> (a, a) : Id_on A"
     1.8 +lemma Id_onI [intro!,no_atp]: "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 @@ -361,7 +361,7 @@
    1.13  
    1.14  subsection {* Domain *}
    1.15  
    1.16 -declare Domain_def [noatp]
    1.17 +declare Domain_def [no_atp]
    1.18  
    1.19  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
    1.20  by (unfold Domain_def) blast
    1.21 @@ -484,7 +484,7 @@
    1.22  
    1.23  subsection {* Image of a set under a relation *}
    1.24  
    1.25 -declare Image_def [noatp]
    1.26 +declare Image_def [no_atp]
    1.27  
    1.28  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
    1.29  by (simp add: Image_def)
    1.30 @@ -495,7 +495,7 @@
    1.31  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
    1.32  by (rule Image_iff [THEN trans]) simp
    1.33  
    1.34 -lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
    1.35 +lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
    1.36  by (unfold Image_def) blast
    1.37  
    1.38  lemma ImageE [elim!]: