# HG changeset patch
# User paulson
# Date 872160803 -7200
# Node ID a64c8fbcd98f8149b762eb7ba5bfc1d0dc1a0aac
# Parent  a11338a5d2d498ae22cbe7cddd139f0c3a0ac88b
Renamed theorems of the form set_of_list_XXX to set_XXX

diff -r a11338a5d2d4 -r a64c8fbcd98f src/HOL/List.ML
--- a/src/HOL/List.ML	Sun Aug 10 12:28:34 1997 +0200
+++ b/src/HOL/List.ML	Thu Aug 21 12:53:23 1997 +0200
@@ -246,37 +246,37 @@
 goal thy "set (xs@ys) = (set xs Un set ys)";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-qed "set_of_list_append";
-Addsimps[set_of_list_append];
+qed "set_append";
+Addsimps[set_append];
 
 goal thy "(x mem xs) = (x: set xs)";
 by (induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Blast_tac 1);
-qed "set_of_list_mem_eq";
+qed "set_mem_eq";
 
 goal thy "set l <= set (x#l)";
 by (Simp_tac 1);
 by (Blast_tac 1);
-qed "set_of_list_subset_Cons";
+qed "set_subset_Cons";
 
 goal thy "(set xs = {}) = (xs = [])";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-qed "set_of_list_empty";
-Addsimps [set_of_list_empty];
+qed "set_empty";
+Addsimps [set_empty];
 
 goal thy "set(rev xs) = set(xs)";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-qed "set_of_list_rev";
-Addsimps [set_of_list_rev];
+qed "set_rev";
+Addsimps [set_rev];
 
 goal thy "set(map f xs) = f``(set xs)";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-qed "set_of_list_map";
-Addsimps [set_of_list_map];
+qed "set_map";
+Addsimps [set_map];
 
 
 (** list_all **)
@@ -331,8 +331,8 @@
 goal thy  "set(concat xs) = Union(set `` set xs)";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-qed"set_of_list_concat";
-Addsimps [set_of_list_concat];
+qed"set_concat";
+Addsimps [set_concat];
 
 goal thy "map f (concat xs) = concat (map (map f) xs)"; 
 by (induct_tac "xs" 1);
@@ -625,7 +625,7 @@
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-qed_spec_mp"set_of_list_take_whileD";
+qed_spec_mp"set_take_whileD";
 
 (** replicate **)
 section "replicate";
diff -r a11338a5d2d4 -r a64c8fbcd98f src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Sun Aug 10 12:28:34 1997 +0200
+++ b/src/HOL/ex/InSort.ML	Thu Aug 21 12:53:23 1997 +0200
@@ -19,11 +19,11 @@
 qed "insort_permutes";
 
 goal thy "set(ins f x xs) = insert x (set xs)";
-by (asm_simp_tac (!simpset addsimps [set_of_list_via_mset]
+by (asm_simp_tac (!simpset addsimps [set_via_mset]
                            setloop (split_tac [expand_if])) 1);
 by (Fast_tac 1);
-qed "set_of_list_ins";
-Addsimps [set_of_list_ins];
+qed "set_ins";
+Addsimps [set_ins];
 
 val prems = goalw InSort.thy [total_def,transf_def]
   "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
diff -r a11338a5d2d4 -r a64c8fbcd98f src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Sun Aug 10 12:28:34 1997 +0200
+++ b/src/HOL/ex/Qsort.ML	Thu Aug 21 12:53:23 1997 +0200
@@ -30,16 +30,16 @@
 qed "qsort_permutes";
 
 goal Qsort.thy "set(qsort le xs) = set xs";
-by(simp_tac (!simpset addsimps [set_of_list_via_mset,qsort_permutes]) 1);
-qed "set_of_list_qsort";
-Addsimps [set_of_list_qsort];
+by(simp_tac (!simpset addsimps [set_via_mset,qsort_permutes]) 1);
+qed "set_qsort";
+Addsimps [set_qsort];
 
 goal List.thy
   "(!x:set[x:xs.P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-qed"Ball_set_of_list_filter";
-Addsimps [Ball_set_of_list_filter];
+qed"Ball_set_filter";
+Addsimps [Ball_set_filter];
 
 goal Qsort.thy
  "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
diff -r a11338a5d2d4 -r a64c8fbcd98f src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Sun Aug 10 12:28:34 1997 +0200
+++ b/src/HOL/ex/Sorting.ML	Thu Aug 21 12:53:23 1997 +0200
@@ -23,7 +23,7 @@
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Fast_tac 1);
-qed "set_of_list_via_mset";
+qed "set_via_mset";
 
 (* Equivalence of two definitions of `sorted' *)