author | paulson |
Mon, 13 Mar 2000 12:42:05 +0100 | |
changeset 8421 | 7156b8e26a17 |
parent 8420 | f37fd19476ca |
child 8422 | 6c6a5410a9bd |
--- 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]);