# HG changeset patch
# User huffman
# Date 1176763034 -7200
# Node ID 296813d7d3069fe428827c81a332db5e1c799fbf
# Parent  c51667189bd3cd0a0f17657d59a3c1d1b9e50227
remove use of pos_boundedE

diff -r c51667189bd3 -r 296813d7d306 src/HOL/Hyperreal/FrechetDeriv.thy
--- a/src/HOL/Hyperreal/FrechetDeriv.thy	Tue Apr 17 00:33:49 2007 +0200
+++ b/src/HOL/Hyperreal/FrechetDeriv.thy	Tue Apr 17 00:37:14 2007 +0200
@@ -67,8 +67,8 @@
 apply (unfold_locales)
 apply (simp only: f.add g.add add_ac)
 apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
-apply (rule f.pos_boundedE, rename_tac Kf)
-apply (rule g.pos_boundedE, rename_tac Kg)
+apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
+apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
 apply (rule_tac x="Kf + Kg" in exI, safe)
 apply (subst right_distrib)
 apply (rule order_trans [OF norm_triangle_ineq])