# HG changeset patch
# User hoelzl
# Date 1435663770 -7200
# Node ID f11e9fd70b7dc33eddcfdf89416b39a67ad98d60
# Parent  79d71bfea3105ce0925fbebf299a4f25f6dabd30
fix tex-output for rel_mset

diff -r 79d71bfea310 -r f11e9fd70b7d src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Jun 29 23:44:53 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Jun 30 13:29:30 2015 +0200
@@ -2472,7 +2472,7 @@
 lemma rel_mset_rel_mset': "rel_mset R M N = rel_mset' R M N"
 using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto
 
-text \<open>The main end product for rel_mset: inductive characterization:\<close>
+text \<open>The main end product for @{const rel_mset}: inductive characterization:\<close>
 theorems rel_mset_induct[case_names empty add, induct pred: rel_mset] =
   rel_mset'.induct[unfolded rel_mset_rel_mset'[symmetric]]