# HG changeset patch
# User haftmann
# Date 1463056733 -7200
# Node ID 40134ddec3bfda530ba9c6cb4c8d48c26842e532
# Parent  f2177f5d2aed353de67a495695e79cace526f710
clarified heading

diff -r f2177f5d2aed -r 40134ddec3bf src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu May 12 09:34:07 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu May 12 14:38:53 2016 +0200
@@ -2066,7 +2066,7 @@
     \<Longrightarrow> (I + K, I + J) \<in> mult r"
 using one_step_implies_mult_aux by blast
 
-subsection \<open>A quasi-recursive characterization\<close>
+subsection \<open>A quasi-executable characterization\<close>
 
 text \<open>
   The decreasing parts \<open>A\<close> and \<open>B\<close> of multisets in a multiset-comparison