# HG changeset patch # User haftmann # Date 1266827060 -3600 # Node ID 975b34b6cf5b71dd1af47687d8050f200a618d34 # Parent 3745987488b2660001edbe76a3e9f394fd64186c# Parent 397295fa83875a4a1ceb9271bd996b880aa18802 merged diff -r 3745987488b2 -r 975b34b6cf5b src/HOL/List.thy --- a/src/HOL/List.thy Mon Feb 22 09:17:49 2010 +0100 +++ b/src/HOL/List.thy Mon Feb 22 09:24:20 2010 +0100 @@ -250,7 +250,7 @@ @{lemma "distinct [2,0,1::nat]" by simp}\\ @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\ @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ -@{lemma "List.insert 3 [0::nat,1,2] = [3, 0,1,2]" by (simp add: List.insert_def)}\\ +@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\ @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ @{lemma "nth [a,b,c,d] 2 = c" by simp}\\ @@ -2900,10 +2900,14 @@ "List.insert x [] = [x]" by simp -lemma set_insert: +lemma set_insert [simp]: "set (List.insert x xs) = insert x (set xs)" by (auto simp add: List.insert_def) +lemma distinct_insert [simp]: + "distinct xs \ distinct (List.insert x xs)" + by (simp add: List.insert_def) + subsubsection {* @{text remove1} *}