src/HOL/ex/MergeSort.thy
changeset 32960 69916a850301
parent 30661 54858c8ad226
child 34055 fdf294ee08b2
     1.1 --- a/src/HOL/ex/MergeSort.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/ex/MergeSort.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    "msort [] = []"
     1.5  | "msort [x] = [x]"
     1.6  | "msort xs = merge (msort (take (size xs div 2) xs))
     1.7 -	                  (msort (drop (size xs div 2) xs))"
     1.8 +                    (msort (drop (size xs div 2) xs))"
     1.9  
    1.10  theorem sorted_msort: "sorted (op \<le>) (msort xs)"
    1.11  by (induct xs rule: msort.induct) simp_all