src/ZF/Induct/Multiset.thy

 apply (simp add: multirel_def)
 apply (rule trancl_mono)
 apply (rule multirel1_mono, auto)
 done
 
-(* Equivalence of multirel with the usual (closure-free) def *)
+(* Equivalence of multirel with the usual (closure-free) definition *)
 
 lemma add_diff_eq: "k \<in> nat ==> 0 < k \<longrightarrow> n #+ k #- 1 = n #+ (k #- 1)"
 by (erule nat_induct, auto)
 
 lemma mdiff_union_single_conv: "[|a \<in> mset_of(J); multiset(I); multiset(J) |]