# HG changeset patch
# User haftmann
# Date 1216056028 -7200
# Node ID e16f4baa3db6db51fbb5f5f272c6c372aec7e0db
# Parent  97ce525f664c7410b82f10dbfc855d64b42febf9
tuned

diff -r 97ce525f664c -r e16f4baa3db6 src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Mon Jul 14 17:51:48 2008 +0200
+++ b/src/HOL/Library/Quicksort.thy	Mon Jul 14 19:20:28 2008 +0200
@@ -17,13 +17,8 @@
 "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
 by pat_completeness auto
 
-termination
-by (relation "measure size")
-   (auto simp: length_filter_le[THEN order_class.le_less_trans])
-
-end
-context linorder
-begin
+termination by (relation "measure size")
+  (auto simp: length_filter_le [THEN order_class.le_less_trans])
 
 lemma quicksort_permutes [simp]:
   "multiset_of (quicksort xs) = multiset_of xs"
diff -r 97ce525f664c -r e16f4baa3db6 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Mon Jul 14 17:51:48 2008 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Mon Jul 14 19:20:28 2008 +0200
@@ -1286,7 +1286,7 @@
 apply (rule ext)+
 by simp
 
-instantiation matrix :: ("{ord, zero}") ord
+instantiation matrix :: ("{zero, ord}") ord
 begin
 
 definition
@@ -1299,7 +1299,7 @@
 
 end
 
-instance matrix :: ("{order, zero}") order
+instance matrix :: ("{zero, order}") order
 apply intro_classes
 apply (simp_all add: le_matrix_def less_def)
 apply (auto)
@@ -1437,7 +1437,7 @@
   apply (auto)
   done  
 
-instantiation matrix :: ("{zero, lattice}") lattice
+instantiation matrix :: ("{lattice, zero}") lattice
 begin
 
 definition [code func del]: "inf = combine_matrix inf"