| changeset 5148 | 74919e8f221c |
| parent 5069 | 3ea049f7979d |
| child 5184 | 9b8547a9496a |
--- a/src/HOL/ex/Qsort.ML Wed Jul 15 14:13:18 1998 +0200 +++ b/src/HOL/ex/Qsort.ML Wed Jul 15 14:19:02 1998 +0200 @@ -49,8 +49,7 @@ qed "sorted_append"; Addsimps [sorted_append]; -Goal - "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; +Goal "[| total(le); transf(le) |] ==> sorted le (qsort le xs)"; by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); by (ALLGOALS Asm_simp_tac); by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);