# HG changeset patch
# User haftmann
# Date 1266831538 -3600
# Node ID 71bca9e4c483840a5da9bef53f6d3666a469068d
# Parent  4f6760122b2aba1978f528fb3bd914abeaf67ebc# Parent  601ba79217e9b40220d11d0fe1f5d0f042cc36e0
merged

diff -r 4f6760122b2a -r 71bca9e4c483 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/List.thy	Mon Feb 22 10:38:58 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 \<Longrightarrow> distinct (List.insert x xs)"
+  by (simp add: List.insert_def)
+
 
 subsubsection {* @{text remove1} *}