--- a/src/HOL/List.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/List.thy Thu Mar 18 12:58:52 2010 +0100
@@ -582,7 +582,7 @@
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
by (induct xs) auto
-lemma append_eq_append_conv [simp, noatp]:
+lemma append_eq_append_conv [simp, no_atp]:
"length xs = length ys \<or> length us = length vs
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
apply (induct xs arbitrary: ys)
@@ -614,7 +614,7 @@
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
using append_same_eq [of "[]"] by auto
-lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
by (induct xs) auto
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
@@ -3928,10 +3928,10 @@
for A :: "'a set"
where
Nil [intro!]: "[]: lists A"
- | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
-
-inductive_cases listsE [elim!,noatp]: "x#l : lists A"
-inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
+ | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
+
+inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
+inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
@@ -3966,15 +3966,15 @@
lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
-lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
by (rule in_listsp_conv_set [THEN iffD1])
-lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
-
-lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
+
+lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
by (rule in_listsp_conv_set [THEN iffD2])
-lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
+lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
lemma lists_UNIV [simp]: "lists UNIV = UNIV"
by auto