src/HOL/List.ML
changeset 9187 68ecc04785f1
parent 9108 9fff97d29837
child 9268 4313b08b6e1b
     1.1 --- a/src/HOL/List.ML	Thu Jun 29 12:14:45 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Jun 29 12:15:08 2000 +0200
     1.3 @@ -477,6 +477,8 @@
     1.4  
     1.5  Goal "set[i..j(] = {k. i <= k & k < j}";
     1.6  by (induct_tac "j" 1);
     1.7 +by (ALLGOALS Asm_simp_tac);
     1.8 +by (etac ssubst 1);
     1.9  by Auto_tac;
    1.10  by (arith_tac 1);
    1.11  qed "set_upt";