# HG changeset patch
# User paulson
# Date 872160910 -7200
# Node ID e530286d48475fdfc32c2a0da679cd64648a7474
# Parent  bc2c363371ee27a6a4a1aaadc10ebd7016de8d67
Renamed set_of_list to set, and relevant theorems too

diff -r bc2c363371ee -r e530286d4847 src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Thu Aug 21 12:54:20 1997 +0200
+++ b/src/HOL/Induct/SList.ML	Thu Aug 21 12:55:10 1997 +0200
@@ -281,7 +281,7 @@
 val [ttl_Nil, ttl_Cons]                 = list_recs ttl_def;
 val [append_Nil3, append_Cons]          = list_recs append_def;
 val [mem_Nil, mem_Cons]                 = list_recs mem_def;
-val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def;
+val [set_Nil, set_Cons]                 = list_recs set_def;
 val [map_Nil, map_Cons]                 = list_recs map_def;
 val [list_case_Nil, list_case_Cons]     = list_recs list_case_def;
 val [filter_Nil, filter_Cons]           = list_recs filter_def;
@@ -291,7 +291,7 @@
    mem_Nil, mem_Cons,
    list_case_Nil, list_case_Cons,
    append_Nil3, append_Cons,
-   set_of_list_Nil, set_of_list_Cons, 
+   set_Nil, set_Cons, 
    map_Nil, map_Cons,
    filter_Nil, filter_Cons];
 
diff -r bc2c363371ee -r e530286d4847 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Thu Aug 21 12:54:20 1997 +0200
+++ b/src/HOL/Induct/SList.thy	Thu Aug 21 12:55:10 1997 +0200
@@ -37,7 +37,7 @@
   null        :: 'a list => bool
   hd          :: 'a list => 'a
   tl,ttl      :: 'a list => 'a list
-  set_of_list :: ('a list => 'a set)
+  set         :: ('a list => 'a set)
   mem         :: ['a, 'a list] => bool                            (infixl 55)
   map         :: ('a=>'b) => ('a list => 'b list)
   "@"         :: ['a list, 'a list] => 'a list                    (infixr 65)
@@ -105,7 +105,7 @@
   (* a total version of tl: *)
   ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
 
-  set_of_list_def "set_of_list xs    == list_rec xs {} (%x l r. insert x r)"
+  set_def       "set xs              == list_rec xs {} (%x l r. insert x r)"
 
   mem_def       "x mem xs            == 
                    list_rec xs False (%y ys r. if y=x then True else r)"
diff -r bc2c363371ee -r e530286d4847 src/HOL/Induct/Term.ML
--- a/src/HOL/Induct/Term.ML	Thu Aug 21 12:54:20 1997 +0200
+++ b/src/HOL/Induct/Term.ML	Thu Aug 21 12:55:10 1997 +0200
@@ -65,7 +65,7 @@
 
 (*Induction for the abstract type 'a term*)
 val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
-    "[| !!x ts. (ALL t: set_of_list ts. R t) ==> R(App x ts)  \
+    "[| !!x ts. (ALL t: set ts. R t) ==> R(App x ts)  \
 \    |] ==> R(t)";
 by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
 by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);