# HG changeset patch
# User haftmann
# Date 1274515969 -7200
# Node ID 322d065ebef7207bd1ccd93729b6b23e9d23c804
# Parent  8f9f3d61ca8c20b02302a70be62c9fdb461949b2
localized properties_for_sort

diff -r 8f9f3d61ca8c -r 322d065ebef7 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri May 21 17:16:16 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat May 22 10:12:49 2010 +0200
@@ -826,7 +826,8 @@
   This lemma shows which properties suffice to show that a function
   @{text "f"} with @{text "f xs = ys"} behaves like sort.
 *}
-lemma properties_for_sort:
+
+lemma (in linorder) properties_for_sort:
   "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
 proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp