diff -r 066bb557570f -r 7619080e49f0 src/HOL/List.thy --- a/src/HOL/List.thy Wed Aug 15 09:02:11 2007 +0200 +++ b/src/HOL/List.thy Wed Aug 15 12:52:56 2007 +0200 @@ -436,7 +436,7 @@ lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" by (induct xs) auto -lemma append_eq_append_conv [simp]: +lemma append_eq_append_conv [simp,noatp]: "!!ys. length xs = length ys \ length us = length vs ==> (xs@us = ys@vs) = (xs=ys \ us=vs)" apply (induct xs) @@ -469,7 +469,7 @@ lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" using append_same_eq [of "[]"] by auto -lemma hd_Cons_tl [simp]: "xs \ [] ==> hd xs # tl xs = xs" +lemma hd_Cons_tl [simp,noatp]: "xs \ [] ==> hd xs # tl xs = xs" by (induct xs) auto lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" @@ -2391,10 +2391,10 @@ for A :: "'a set" where Nil [intro!]: "[]: lists A" - | Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A" - -inductive_cases listsE [elim!]: "x#l : lists A" -inductive_cases listspE [elim!]: "listsp A (x # l)" + | 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)" lemma listsp_mono [mono]: "A \ B ==> listsp A \ listsp B" by (clarify, erule listsp.induct, blast+) @@ -2429,15 +2429,15 @@ lemmas in_lists_conv_set = in_listsp_conv_set [to_set] -lemma in_listspD [dest!]: "listsp A xs ==> \x\set xs. A x" +lemma in_listspD [dest!,noatp]: "listsp A xs ==> \x\set xs. A x" by (rule in_listsp_conv_set [THEN iffD1]) -lemmas in_listsD [dest!] = in_listspD [to_set] - -lemma in_listspI [intro!]: "\x\set xs. A x ==> listsp A xs" +lemmas in_listsD [dest!,noatp] = in_listspD [to_set] + +lemma in_listspI [intro!,noatp]: "\x\set xs. A x ==> listsp A xs" by (rule in_listsp_conv_set [THEN iffD2]) -lemmas in_listsI [intro!] = in_listspI [to_set] +lemmas in_listsI [intro!,noatp] = in_listspI [to_set] lemma lists_UNIV [simp]: "lists UNIV = UNIV" by auto