clarified heading
authorhaftmann
Thu May 12 14:38:53 2016 +0200 (2016-05-12 ago)
changeset 6308940134ddec3bf
parent 63088 f2177f5d2aed
child 63090 7aa9ac5165e4
clarified heading
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu May 12 09:34:07 2016 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu May 12 14:38:53 2016 +0200
     1.3 @@ -2066,7 +2066,7 @@
     1.4      \<Longrightarrow> (I + K, I + J) \<in> mult r"
     1.5  using one_step_implies_mult_aux by blast
     1.6  
     1.7 -subsection \<open>A quasi-recursive characterization\<close>
     1.8 +subsection \<open>A quasi-executable characterization\<close>
     1.9  
    1.10  text \<open>
    1.11    The decreasing parts \<open>A\<close> and \<open>B\<close> of multisets in a multiset-comparison