fixed the goal statement of sorted_qsort
authorpaulson
Mon Mar 13 12:42:05 2000 +0100 (2000-03-13)
changeset 84217156b8e26a17
parent 8420 f37fd19476ca
child 8422 6c6a5410a9bd
fixed the goal statement of sorted_qsort
src/HOL/ex/Qsort.ML
     1.1 --- a/src/HOL/ex/Qsort.ML	Mon Mar 13 12:25:52 2000 +0100
     1.2 +++ b/src/HOL/ex/Qsort.ML	Mon Mar 13 12:42:05 2000 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  qed "set_qsort";
     1.5  Addsimps [set_qsort];
     1.6  
     1.7 -Goal "total(le) & transf(le) --> sorted le (qsort(le,xs))";
     1.8 +Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
     1.9  by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
    1.10  by (ALLGOALS Asm_simp_tac);
    1.11  by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);