1.1 --- a/src/HOL/Library/Sublist_Order.thy	Wed Jul 02 17:34:45 2014 +0200
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Thu Jul 03 09:55:15 2014 +0200
     1.3 @@ -48,21 +48,21 @@
     1.4  qed
     1.5  
     1.6  lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
     1.7 -  list_hembeq.induct [of "op =", folded less_eq_list_def]
     1.8 -lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def]
     1.9 +  list_emb.induct [of "op =", folded less_eq_list_def]
    1.10 +lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
    1.11  lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
    1.12  lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
    1.13  lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
    1.14 -lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def]
    1.15 +lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
    1.16  
    1.17  lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
    1.18 -  by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
    1.19 +  by (metis list_emb_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
    1.20  
    1.21  lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
    1.22 -  by (metis less_eq_list_def list_hembeq_Nil order_less_le)
    1.23 +  by (metis less_eq_list_def list_emb_Nil order_less_le)
    1.24  
    1.25  lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
    1.26 -  by (metis list_hembeq_Nil less_eq_list_def less_list_def)
    1.27 +  by (metis list_emb_Nil less_eq_list_def less_list_def)
    1.28  
    1.29  lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    1.30    by (unfold less_le less_eq_list_def) (auto)