# HG changeset patch
# User paulson
# Date 939809002 -7200
# Node ID 03fd460cb8b80737b3f62364477516c22bbc598d
# Parent  5aca258fedcf8965a8bbdd403b2229bd6340ea1a
new theorem set_mono

diff -r 5aca258fedcf -r 03fd460cb8b8 src/HOL/UNITY/GenPrefix.ML
--- 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 **)