--- 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"
--- 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"