new theorem set_mono

--- a/src/HOL/UNITY/GenPrefix.ML	Tue Oct 12 19:14:06 1999 +0200
+++ b/src/HOL/UNITY/GenPrefix.ML	Wed Oct 13 12:03:22 1999 +0200
@@ -226,6 +226,12 @@
 by Auto_tac;
 qed "prefix_less_le";
 
+(*Monotonicity of "set" operator WRT prefix*)
+Goalw [prefix_def] "xs <= ys ==> set xs <= set ys";
+by (etac genPrefix.induct 1);
+by Auto_tac;
+qed "set_mono";
+
 
 (** recursion equations **)