diff -r 7a3724078363 -r c32254ab1901 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Tue Nov 07 14:52:27 2017 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Tue Nov 07 15:16:40 2017 +0100
@@ -166,8 +166,7 @@
 
 end
 
-lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
-  "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
   unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
 
 lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
@@ -178,8 +177,8 @@
   unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
   by (simp add: less_le_not_le subseteq_mset_def)
 
-lemma le_multiset_right_total:
-  shows "M < add_mset x M"
+(* FIXME: "le" should be "less" in this and other names *)
+lemma le_multiset_right_total: "M < add_mset x M"
   unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
 
 lemma less_eq_multiset_empty_left[simp]:
@@ -190,16 +189,18 @@
   unfolding less_multiset\<^sub>H\<^sub>O
   by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
 
-lemma less_eq_multiset_empty_right[simp]:
-  "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
+lemma less_eq_multiset_empty_right[simp]: "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
   by (metis less_eq_multiset_empty_left antisym)
 
+(* FIXME: "le" should be "less" in this and other names *)
 lemma le_multiset_empty_left[simp]: "M \<noteq> {#} \<Longrightarrow> {#} < M"
   by (simp add: less_multiset\<^sub>H\<^sub>O)
 
+(* FIXME: "le" should be "less" in this and other names *)
 lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
   using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
 
+(* FIXME: "le" should be "less" in this and other names *)
 lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
   by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)