| changeset 171 | 16c4ea954511 |
| parent 62 | 32a83e3ad5a4 |
| child 195 | df6b3bd14dcb |
--- a/ex/Qsort.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/ex/Qsort.ML Mon Nov 21 17:50:34 1994 +0100 @@ -27,7 +27,7 @@ goal HOL.thy "((~P --> Q) & (P --> Q)) = Q"; by(fast_tac HOL_cs 1); -val lemma = result(); +qed "lemma"; goal Qsort.thy "(Alls x:qsort(le,xs).P(x)) = (Alls x:xs.P(x))"; by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);