--- 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];
--- 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)"
--- 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);