| changeset 5143 | b94cd208f073 |
| parent 5069 | 3ea049f7979d |
| child 5184 | 9b8547a9496a |
--- a/src/HOL/ex/InSort.ML Tue Jul 14 13:33:12 1998 +0200 +++ b/src/HOL/ex/InSort.ML Wed Jul 15 10:15:13 1998 +0200 @@ -32,7 +32,7 @@ qed "sorted_ins"; Addsimps [sorted_ins]; -Goal "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)"; +Goal "[| total(f); transf(f) |] ==> sorted f (insort f xs)"; by (list.induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "sorted_insort";