src/HOL/Library/Lattice_Algebras.thy
changeset 35828 46cfc4b8112e
parent 35040 e42e7f133d94
child 36976 e78d1e06d855
     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Wed Mar 17 19:37:44 2010 +0100
     1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 18 12:58:52 2010 +0100
     1.3 @@ -163,16 +163,16 @@
     1.4  lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
     1.5  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
     1.6  
     1.7 -lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
     1.8 +lemma pprt_eq_id [simp, no_atp]: "0 \<le> x \<Longrightarrow> pprt x = x"
     1.9    by (simp add: pprt_def sup_aci sup_absorb1)
    1.10  
    1.11 -lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
    1.12 +lemma nprt_eq_id [simp, no_atp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
    1.13    by (simp add: nprt_def inf_aci inf_absorb1)
    1.14  
    1.15 -lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
    1.16 +lemma pprt_eq_0 [simp, no_atp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
    1.17    by (simp add: pprt_def sup_aci sup_absorb2)
    1.18  
    1.19 -lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
    1.20 +lemma nprt_eq_0 [simp, no_atp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
    1.21    by (simp add: nprt_def inf_aci inf_absorb2)
    1.22  
    1.23  lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
    1.24 @@ -197,10 +197,10 @@
    1.25  apply (erule sup_0_imp_0)
    1.26  done
    1.27  
    1.28 -lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
    1.29 +lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
    1.30  by (rule, erule inf_0_imp_0) simp
    1.31  
    1.32 -lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
    1.33 +lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
    1.34  by (rule, erule sup_0_imp_0) simp
    1.35  
    1.36  lemma zero_le_double_add_iff_zero_le_single_add [simp]:
    1.37 @@ -295,10 +295,10 @@
    1.38  lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
    1.39  unfolding le_iff_inf by (simp add: nprt_def inf_commute)
    1.40  
    1.41 -lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
    1.42 +lemma pprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
    1.43  unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
    1.44  
    1.45 -lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
    1.46 +lemma nprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
    1.47  unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
    1.48  
    1.49  end