# 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);