# HG changeset patch
# User nipkow
# Date 1536813461 -7200
# Node ID b1d106c1edac6aacff142c0436dde133d70535ad
# Parent  807099160468d56092bb24ed87edcac755ee6b5e# Parent  caedabd2771c0e18fb817613567ed3ca20cf66af
merged

diff -r 807099160468 -r b1d106c1edac src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Sep 12 22:33:26 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 13 06:37:41 2018 +0200
@@ -2652,7 +2652,7 @@
     @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
   using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
 
-text \<open>A stable parametrized quicksort\<close>
+text \<open>A stable parameterized quicksort\<close>
 
 definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
   "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"