src/HOL/Hyperreal/Transcendental.ML

--- a/src/HOL/Hyperreal/Transcendental.ML	Tue Jan 13 10:37:52 2004 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML	Wed Jan 14 00:13:04 2004 +0100
@@ -1601,8 +1601,6 @@
 by (ALLGOALS(Asm_simp_tac));
 by (TRYALL(rtac real_less_trans));
 by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc] delsimps [fact_Suc]));
-by (res_inst_tac [("y","0")] order_less_le_trans 1);
-by (ALLGOALS(Asm_simp_tac));
 qed "sin_gt_zero";
 
 Goal "[|0 < x; x < 2 |] ==> 0 < sin x";