# HG changeset patch
# User paulson
# Date 907749090 -7200
# Node ID 76a8c72e3fd499864fed817b5790e1740dc3a81b
# Parent  721671c68324bb3091bc4a687c6b50e2133aac5c
new theorems

diff -r 721671c68324 -r 76a8c72e3fd4 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Wed Oct 07 10:31:07 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML	Wed Oct 07 10:31:30 1998 +0200
@@ -87,3 +87,14 @@
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "prefix_append";
+
+Goalw [prefix_def]
+  "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
+by (auto_tac(claset(), simpset() addsimps [nth_append]));
+by (exhaust_tac "ys" 1);
+by Auto_tac;
+qed "append_one_prefix";
+
+Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
+by Auto_tac;
+qed "prefix_length_le";