localized properties_for_sort
authorhaftmann
Sat May 22 10:12:49 2010 +0200 (2010-05-22)
changeset 37074322d065ebef7
parent 37055 8f9f3d61ca8c
child 37075 a680ce27aa56
localized properties_for_sort
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri May 21 17:16:16 2010 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat May 22 10:12:49 2010 +0200
     1.3 @@ -826,7 +826,8 @@
     1.4    This lemma shows which properties suffice to show that a function
     1.5    @{text "f"} with @{text "f xs = ys"} behaves like sort.
     1.6  *}
     1.7 -lemma properties_for_sort:
     1.8 +
     1.9 +lemma (in linorder) properties_for_sort:
    1.10    "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
    1.11  proof (induct xs arbitrary: ys)
    1.12    case Nil then show ?case by simp