--- a/src/HOL/Library/Subseq_Order.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Library/Subseq_Order.thy Wed Jan 10 15:25:09 2018 +0100
@@ -41,12 +41,12 @@
qed
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
- list_emb.induct [of "op =", folded less_eq_list_def]
-lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
+ list_emb.induct [of "(=)", folded less_eq_list_def]
+lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "(=)", folded less_eq_list_def]
lemmas le_list_Cons2_iff [simp, code] = subseq_Cons2_iff [folded less_eq_list_def]
lemmas le_list_map = subseq_map [folded less_eq_list_def]
lemmas le_list_filter = subseq_filter [folded less_eq_list_def]
-lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
+lemmas le_list_length = list_emb_length [of "(=)", folded less_eq_list_def]
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def)