--- a/src/HOL/Product_Type.thy Thu Mar 18 13:57:00 2010 +0100
+++ b/src/HOL/Product_Type.thy Thu Mar 18 13:59:20 2010 +0100
@@ -46,7 +46,7 @@
where
"() = Abs_unit True"
-lemma unit_eq [noatp]: "u = ()"
+lemma unit_eq [no_atp]: "u = ()"
by (induct u) (simp add: unit_def Unity_def)
text {*
@@ -78,7 +78,7 @@
f} rather than by @{term [source] "%u. f ()"}.
*}
-lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
by (rule ext) simp
instantiation unit :: default
@@ -497,7 +497,7 @@
lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
by (subst surjective_pairing, rule split_conv)
-lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
+lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
-- {* For use with @{text split} and the Simplifier. *}
by (insert surj_pair [of p], clarify, simp)
@@ -508,7 +508,7 @@
current goal contains one of those constants.
*}
-lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
+lemma split_split_asm [no_atp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
by (subst split_split, simp)
@@ -582,10 +582,10 @@
Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
*}
-lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
+lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
by (rule ext) fast
-lemma split_eta_SetCompr2 [simp,noatp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
+lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
by (rule ext) fast
lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
@@ -947,11 +947,11 @@
-- {* Suggested by Pierre Chartier *}
by blast
-lemma split_paired_Ball_Sigma [simp,noatp]:
+lemma split_paired_Ball_Sigma [simp,no_atp]:
"(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
by blast
-lemma split_paired_Bex_Sigma [simp,noatp]:
+lemma split_paired_Bex_Sigma [simp,no_atp]:
"(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
by blast