# HG changeset patch
# User paulson
# Date 952947725 -3600
# Node ID 7156b8e26a172cc469c5577b95737a7a58218fab
# Parent  f37fd19476ca7485ebbd3467821b8894c35589bf
fixed the goal statement of sorted_qsort

diff -r f37fd19476ca -r 7156b8e26a17 src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Mon Mar 13 12:25:52 2000 +0100
+++ b/src/HOL/ex/Qsort.ML	Mon Mar 13 12:42:05 2000 +0100
@@ -20,7 +20,7 @@
 qed "set_qsort";
 Addsimps [set_qsort];
 
-Goal "total(le) & transf(le) --> sorted le (qsort(le,xs))";
+Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
 by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);