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