1.1 --- a/src/HOL/List.ML	Wed Feb 13 10:48:29 2002 +0100
     1.2 +++ b/src/HOL/List.ML	Thu Feb 14 11:50:52 2002 +0100
     1.3 @@ -1277,8 +1277,14 @@
     1.4  qed_spec_mp "take_equalityI";
     1.5  
     1.6  
     1.7 -(** nodups & remdups **)
     1.8 -section "nodups & remdups";
     1.9 +(** distinct & remdups **)
    1.10 +section "distinct & remdups";
    1.11 +
    1.12 +Goal  "distinct(xs@ys) = (distinct xs & distinct ys & set xs Int set ys = {})";
    1.13 +by(induct_tac "xs" 1);
    1.14 +by Auto_tac;
    1.15 +qed "distinct_append";
    1.16 +Addsimps [distinct_append];
    1.17  
    1.18  Goal "set(remdups xs) = set xs";
    1.19  by (induct_tac "xs" 1);
    1.20 @@ -1287,15 +1293,15 @@
    1.21  qed "set_remdups";
    1.22  Addsimps [set_remdups];
    1.23  
    1.24 -Goal "nodups(remdups xs)";
    1.25 +Goal "distinct(remdups xs)";
    1.26  by (induct_tac "xs" 1);
    1.27  by Auto_tac;
    1.28 -qed "nodups_remdups";
    1.29 +qed "distinct_remdups";
    1.30  
    1.31 -Goal "nodups xs --> nodups (filter P xs)";
    1.32 +Goal "distinct xs --> distinct (filter P xs)";
    1.33  by (induct_tac "xs" 1);
    1.34  by Auto_tac;
    1.35 -qed_spec_mp "nodups_filter";
    1.36 +qed_spec_mp "distinct_filter";
    1.37  
    1.38  (** replicate **)
    1.39  section "replicate";

     2.1 --- a/src/HOL/List.thy	Wed Feb 13 10:48:29 2002 +0100
     2.2 +++ b/src/HOL/List.thy	Thu Feb 14 11:50:52 2002 +0100
     2.3 @@ -31,8 +31,8 @@
     2.4    rev         :: 'a list => 'a list
     2.5    zip	      :: "'a list => 'b list => ('a * 'b) list"
     2.6    upt         :: nat => nat => nat list                   ("(1[_../_'(])")
     2.7 -  remdups     :: 'a list => 'a list
     2.8 -  null, nodups :: "'a list => bool"
     2.9 +  remdups     :: "'a list => 'a list"
    2.10 +  null, "distinct" :: "'a list => bool"
    2.11    replicate   :: nat => 'a => 'a list
    2.12  
    2.13  nonterminals
    2.14 @@ -158,8 +158,8 @@
    2.15    upt_0   "[i..0(] = []"
    2.16    upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
    2.17  primrec
    2.18 -  "nodups []     = True"
    2.19 -  "nodups (x#xs) = (x ~: set xs & nodups xs)"
    2.20 +  "distinct []     = True"
    2.21 +  "distinct (x#xs) = (x ~: set xs & distinct xs)"
    2.22  primrec
    2.23    "remdups [] = []"
    2.24    "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"