# HG changeset patch
# User nipkow
# Date 1536584936 -7200
# Node ID 2881f6cccc67bf92afe4ba85b0730ea4011b5d54
# Parent  1254f3e57fed3c7933e1b3adbf02343f87b59fd1
tuned

diff -r 1254f3e57fed -r 2881f6cccc67 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Sun Sep 09 17:40:12 2018 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy	Mon Sep 10 15:08:56 2018 +0200
@@ -128,25 +128,25 @@
 proof(induction xs rule: msort.induct)
   case (1 xs)
   let ?n = "length xs"
-  let ?xs1 = "take (?n div 2) xs"
-  let ?xs2 = "drop (?n div 2) xs"
+  let ?ys = "take (?n div 2) xs"
+  let ?zs = "drop (?n div 2) xs"
   show ?case
   proof cases
     assume "?n \<le> 1"
     thus ?thesis by(simp add: msort.simps[of xs])
   next
     assume "\<not> ?n \<le> 1"
-    hence "mset (msort xs) = mset (msort ?xs1) + mset (msort ?xs2)"
+    hence "mset (msort xs) = mset (msort ?ys) + mset (msort ?zs)"
       by(simp add: msort.simps[of xs] mset_merge)
-    also have "\<dots> = mset ?xs1 + mset ?xs2"
+    also have "\<dots> = mset ?ys + mset ?zs"
       using \<open>\<not> ?n \<le> 1\<close> by(simp add: "1.IH")
-    also have "\<dots> = mset (?xs1 @ ?xs2)" by (simp del: append_take_drop_id)
+    also have "\<dots> = mset (?ys @ ?zs)" by (simp del: append_take_drop_id)
     also have "\<dots> = mset xs" by simp
     finally show ?thesis .
   qed
 qed
 
-text \<open>Via the previous lemma or directtly:\<close>
+text \<open>Via the previous lemma or directly:\<close>
 
 lemma set_merge: "set(merge xs ys) = set xs \<union> set ys"
 by (metis mset_merge set_mset_mset set_mset_union)
@@ -157,7 +157,7 @@
 lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> sorted ys)"
 by(induction xs ys rule: merge.induct) (auto simp: set_merge)
 
-lemma "sorted (msort xs)"
+lemma sorted_msort: "sorted (msort xs)"
 proof(induction xs rule: msort.induct)
   case (1 xs)
   let ?n = "length xs"
@@ -168,7 +168,7 @@
   next
     assume "\<not> ?n \<le> 1"
     thus ?thesis using "1.IH"
-      by(simp add: sorted_merge  msort.simps[of xs] mset_merge)
+      by(simp add: sorted_merge msort.simps[of xs])
   qed
 qed