summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Multiset.thy

changeset 37074 | 322d065ebef7 |

parent 36903 | 489c1fbbb028 |

child 37107 | 1535aa1c943a |

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