# HG changeset patch
# User Christian Sternagel
# Date 1346309043 -32400
# Node ID fdc301f592c439475485aac963121cf742474a29
# Parent  5eddc9aaebf1a5cba794d34e595c917c5f998399
forgot to add lemmas

diff -r 5eddc9aaebf1 -r fdc301f592c4 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Thu Aug 30 13:44:15 2012 +0900
+++ b/src/HOL/Library/Sublist_Order.thy	Thu Aug 30 15:44:03 2012 +0900
@@ -47,6 +47,14 @@
   thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
 qed
 
+lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
+  emb.induct [of "op =", folded less_eq_list_def]
+lemmas less_eq_list_drop = emb.emb_Cons [of "op =", folded less_eq_list_def]
+lemmas le_list_Cons2_iff [simp, code] = sub_Cons2_iff [folded less_eq_list_def]
+lemmas le_list_map = sub_map [folded less_eq_list_def]
+lemmas le_list_filter = sub_filter [folded less_eq_list_def]
+lemmas le_list_length = emb_length [of "op =", folded less_eq_list_def]
+
 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
   by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)