# HG changeset patch
# User nipkow
# Date 1113494243 -7200
# Node ID faa48c5b14021b83e45fc24d4aa169dade2e344f
# Parent  29ae73d8a84e09b494f933f9cc68253a8491c6ca
Added thm names

diff -r 29ae73d8a84e -r faa48c5b1402 src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Thu Apr 14 17:57:04 2005 +0200
+++ b/src/HOL/ex/MergeSort.thy	Thu Apr 14 17:57:23 2005 +0200
@@ -16,17 +16,18 @@
 "merge(xs,[]) = xs"
 "merge([],ys) = ys"
 
-lemma [simp]: "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
+lemma multiset_of_merge[simp]:
+ "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
 apply(induct xs ys rule: merge.induct)
 apply (auto simp: union_ac)
 done
 
-lemma [simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
+lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
 apply(induct xs ys rule: merge.induct)
 apply auto
 done
 
-lemma [simp]:
+lemma sorted_merge[simp]:
  "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
 apply(induct xs ys rule: merge.induct)
 apply(simp_all add:ball_Un linorder_not_le order_less_le)
@@ -40,10 +41,10 @@
 "msort xs = merge(msort(take (size xs div 2) xs),
                   msort(drop (size xs div 2) xs))"
 
-lemma "sorted op <= (msort xs)"
+lemma sorted_msort: "sorted op <= (msort xs)"
 by (induct xs rule: msort.induct) simp_all
 
-lemma "multiset_of (msort xs) = multiset_of xs"
+lemma multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
 apply (induct xs rule: msort.induct)
   apply simp
  apply simp