# HG changeset patch
# User nipkow
# Date 1013683852 -3600
# Node ID d25b43743e10f6dd7a122b8c26680edd774dbf3f
# Parent  75ca1bf5ae122fd5e63b7ebc539759c2b1148b80
nodups -> distinct

diff -r 75ca1bf5ae12 -r d25b43743e10 src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Feb 13 10:48:29 2002 +0100
+++ b/src/HOL/List.ML	Thu Feb 14 11:50:52 2002 +0100
@@ -1277,8 +1277,14 @@
 qed_spec_mp "take_equalityI";
 
 
-(** nodups & remdups **)
-section "nodups & remdups";
+(** distinct & remdups **)
+section "distinct & remdups";
+
+Goal  "distinct(xs@ys) = (distinct xs & distinct ys & set xs Int set ys = {})";
+by(induct_tac "xs" 1);
+by Auto_tac;
+qed "distinct_append";
+Addsimps [distinct_append];
 
 Goal "set(remdups xs) = set xs";
 by (induct_tac "xs" 1);
@@ -1287,15 +1293,15 @@
 qed "set_remdups";
 Addsimps [set_remdups];
 
-Goal "nodups(remdups xs)";
+Goal "distinct(remdups xs)";
 by (induct_tac "xs" 1);
 by Auto_tac;
-qed "nodups_remdups";
+qed "distinct_remdups";
 
-Goal "nodups xs --> nodups (filter P xs)";
+Goal "distinct xs --> distinct (filter P xs)";
 by (induct_tac "xs" 1);
 by Auto_tac;
-qed_spec_mp "nodups_filter";
+qed_spec_mp "distinct_filter";
 
 (** replicate **)
 section "replicate";
diff -r 75ca1bf5ae12 -r d25b43743e10 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 13 10:48:29 2002 +0100
+++ b/src/HOL/List.thy	Thu Feb 14 11:50:52 2002 +0100
@@ -31,8 +31,8 @@
   rev         :: 'a list => 'a list
   zip	      :: "'a list => 'b list => ('a * 'b) list"
   upt         :: nat => nat => nat list                   ("(1[_../_'(])")
-  remdups     :: 'a list => 'a list
-  null, nodups :: "'a list => bool"
+  remdups     :: "'a list => 'a list"
+  null, "distinct" :: "'a list => bool"
   replicate   :: nat => 'a => 'a list
 
 nonterminals
@@ -158,8 +158,8 @@
   upt_0   "[i..0(] = []"
   upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
 primrec
-  "nodups []     = True"
-  "nodups (x#xs) = (x ~: set xs & nodups xs)"
+  "distinct []     = True"
+  "distinct (x#xs) = (x ~: set xs & distinct xs)"
 primrec
   "remdups [] = []"
   "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"