| changeset 6055 | fdf4638bf726 |
| parent 5983 | 79e301a6a51b |
| child 6058 | a9600c47ace3 |
--- a/src/HOL/List.ML Mon Dec 28 17:03:47 1998 +0100 +++ b/src/HOL/List.ML Mon Jan 04 15:07:47 1999 +0100 @@ -858,7 +858,6 @@ by (induct_tac "ns" 1); by (Simp_tac 1); by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [trans_le_add1]) 1); qed_spec_mp "start_le_sum"; Goal "n : set ns ==> n <= foldl op+ 0 ns";