src/HOL/ex/Qsort.ML
changeset 5278 a903b66822e2
parent 5184 9b8547a9496a
child 6434 f2a2a40e56c8
     1.1 --- a/src/HOL/ex/Qsort.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/ex/Qsort.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -41,8 +41,7 @@
     1.4  qed"Ball_set_filter";
     1.5  Addsimps [Ball_set_filter];
     1.6  
     1.7 -Goal
     1.8 - "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
     1.9 +Goal "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
    1.10  \                     (!x:set xs. !y:set ys. le x y))";
    1.11  by (induct_tac "xs" 1);
    1.12  by (ALLGOALS Asm_simp_tac);