src/HOL/List.thy

--- a/src/HOL/List.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/List.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -39,6 +39,8 @@
 
 setup {* Sign.parent_path *}
 
+lemmas set_simps = list.set (* legacy *)
+
 syntax
   -- {* list Enumeration *}
   "_list" :: "args => 'a list"    ("[(_)]")
@@ -54,16 +56,9 @@
 "last (x # xs) = (if xs = [] then x else last xs)"
 
 primrec butlast :: "'a list \<Rightarrow> 'a list" where
-"butlast []= []" |
+"butlast [] = []" |
 "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
 
-declare list.set[simp del, code del]
-
-lemma set_simps[simp, code, code_post]:
-  "set [] = {}"
-  "set (x # xs) = insert x (set xs)"
-by (simp_all add: list.set)
-
 lemma set_rec: "set xs = rec_list {} (\<lambda>x _. insert x) xs"
   by (induct xs) auto
 
@@ -575,7 +570,7 @@
 
 fun simproc ctxt redex =
   let
-    val set_Nil_I = @{thm trans} OF [@{thm set_simps(1)}, @{thm empty_def}]
+    val set_Nil_I = @{thm trans} OF [@{thm list.set(1)}, @{thm empty_def}]
     val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
     val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
     val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
@@ -1255,6 +1250,8 @@
 
 subsubsection {* @{const set} *}
 
+declare list.set[code_post]  --"pretty output"
+
 lemma finite_set [iff]: "finite (set xs)"
 by (induct xs) auto
 
@@ -1404,7 +1401,7 @@
 
 
 lemma finite_list: "finite A ==> EX xs. set xs = A"
-  by (erule finite_induct) (auto simp add: set_simps(2) [symmetric] simp del: set_simps(2))
+  by (erule finite_induct) (auto simp add: list.set(2)[symmetric] simp del: list.set(2))
 
 lemma card_length: "card (set xs) \<le> length xs"
 by (induct xs) (auto simp add: card_insert_if)