src/HOL/Library/Multiset.thy
changeset 60613 f11e9fd70b7d
parent 60608 c5cbd90bd94e
child 60678 17ba2df56dee
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Jun 29 23:44:53 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jun 30 13:29:30 2015 +0200
     1.3 @@ -2472,7 +2472,7 @@
     1.4  lemma rel_mset_rel_mset': "rel_mset R M N = rel_mset' R M N"
     1.5  using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto
     1.6  
     1.7 -text \<open>The main end product for rel_mset: inductive characterization:\<close>
     1.8 +text \<open>The main end product for @{const rel_mset}: inductive characterization:\<close>
     1.9  theorems rel_mset_induct[case_names empty add, induct pred: rel_mset] =
    1.10    rel_mset'.induct[unfolded rel_mset_rel_mset'[symmetric]]
    1.11