src/HOL/Product_Type.thy
changeset 35831 e31ec41a551b
parent 35822 67e4de90d2c2
parent 35828 46cfc4b8112e
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Product_Type.thy	Thu Mar 18 13:57:00 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 18 13:59:20 2010 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4  where
     1.5    "() = Abs_unit True"
     1.6  
     1.7 -lemma unit_eq [noatp]: "u = ()"
     1.8 +lemma unit_eq [no_atp]: "u = ()"
     1.9    by (induct u) (simp add: unit_def Unity_def)
    1.10  
    1.11  text {*
    1.12 @@ -78,7 +78,7 @@
    1.13    f} rather than by @{term [source] "%u. f ()"}.
    1.14  *}
    1.15  
    1.16 -lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
    1.17 +lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
    1.18    by (rule ext) simp
    1.19  
    1.20  instantiation unit :: default
    1.21 @@ -497,7 +497,7 @@
    1.22  lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
    1.23    by (subst surjective_pairing, rule split_conv)
    1.24  
    1.25 -lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
    1.26 +lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
    1.27    -- {* For use with @{text split} and the Simplifier. *}
    1.28    by (insert surj_pair [of p], clarify, simp)
    1.29  
    1.30 @@ -508,7 +508,7 @@
    1.31    current goal contains one of those constants.
    1.32  *}
    1.33  
    1.34 -lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
    1.35 +lemma split_split_asm [no_atp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
    1.36  by (subst split_split, simp)
    1.37  
    1.38  
    1.39 @@ -582,10 +582,10 @@
    1.40    Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
    1.41  *}
    1.42  
    1.43 -lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
    1.44 +lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
    1.45    by (rule ext) fast
    1.46  
    1.47 -lemma split_eta_SetCompr2 [simp,noatp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
    1.48 +lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
    1.49    by (rule ext) fast
    1.50  
    1.51  lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
    1.52 @@ -947,11 +947,11 @@
    1.53    -- {* Suggested by Pierre Chartier *}
    1.54    by blast
    1.55  
    1.56 -lemma split_paired_Ball_Sigma [simp,noatp]:
    1.57 +lemma split_paired_Ball_Sigma [simp,no_atp]:
    1.58      "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
    1.59    by blast
    1.60  
    1.61 -lemma split_paired_Bex_Sigma [simp,noatp]:
    1.62 +lemma split_paired_Bex_Sigma [simp,no_atp]:
    1.63      "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
    1.64    by blast
    1.65