diff -r 32892a8ecb15 -r 63e53327f5e5 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Fri May 21 10:47:07 1999 +0200
+++ b/src/HOL/Lex/Prefix.ML	Fri May 21 10:50:04 1999 +0200
@@ -21,6 +21,11 @@
 by (Asm_full_simp_tac 1);
 qed "prefix_antisym";
 
+Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)";
+by Auto_tac;
+qed "prefix_less_le";
+
+
 (** recursion equations **)
 
 Goalw [prefix_def] "[] <= xs";
@@ -98,3 +103,7 @@
 Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
 by Auto_tac;
 qed "prefix_length_le";
+
+Goal "mono length";
+by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1);
+qed "mono_length";