changeset 14329 | ff3210fe968f |
parent 14305 | f17ca9f6dc8c |
child 14334 | 6137d24eef79 |
--- a/src/HOL/Hyperreal/Integration.ML Wed Dec 24 08:54:30 2003 +0100 +++ b/src/HOL/Hyperreal/Integration.ML Thu Dec 25 22:48:32 2003 +0100 @@ -183,7 +183,7 @@ by (dres_inst_tac [("x","psize D - Suc n")] spec 2); by (thin_tac "ALL n. psize D <= n --> D n = b" 2); by (Asm_full_simp_tac 2); -by (Blast_tac 1); +by (arith_tac 1); qed "partition_ub"; Goal "[| partition(a,b) D; n < psize D |] ==> D(n) < b";