| changeset 8421 | 7156b8e26a17 |
| parent 8414 | 5983668cac15 |
| child 8590 | 89675b444abe |
--- 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]);