# HG changeset patch
# User paulson
# Date 1192177489 -7200
# Node ID a339b33adfaff6a1ff318767814967dee352241c
# Parent  730d74336b4dca69d4e18f664626a43eca16fb55
metis calls

diff -r 730d74336b4d -r a339b33adfaf src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Oct 12 08:31:57 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Oct 12 10:24:49 2007 +0200
@@ -109,15 +109,8 @@
 apply (rule DERIV_unique)
 prefer 2 apply assumption
 apply force
-apply (subgoal_tac "\<forall>ta. 0 \<le> ta & ta \<le> t --> (difg (Suc n)) differentiable ta")
-apply (simp add: differentiable_def)
-apply (blast dest!: DERIV_isCont)
-apply (simp add: differentiable_def, clarify)
-apply (rule_tac x = "difg (Suc (Suc n)) ta" in exI)
-apply force
-apply (simp add: differentiable_def, clarify)
-apply (rule_tac x = "difg (Suc (Suc n)) x" in exI)
-apply force
+apply (metis DERIV_isCont dlo_simps(4) dlo_simps(9) less_trans_Suc nat_less_le not_less_eq real_le_trans)
+apply (metis Suc_less_eq differentiableI dlo_simps(7) dlo_simps(8) dlo_simps(9)   real_le_trans xt1(8))
 done
 
 lemma Maclaurin:
@@ -183,15 +176,8 @@
 apply force
 apply (rule allI, induct_tac "ma")
 apply (rule impI, rule Rolle, assumption, simp, simp)
-apply (subgoal_tac "\<forall>t. 0 \<le> t & t \<le> h --> g differentiable t")
-apply (simp add: differentiable_def)
-apply (blast dest: DERIV_isCont)
-apply (simp add: differentiable_def, clarify)
-apply (rule_tac x = "difg (Suc 0) t" in exI)
-apply force
-apply (simp add: differentiable_def, clarify)
-apply (rule_tac x = "difg (Suc 0) x" in exI)
-apply force
+apply (metis DERIV_isCont zero_less_Suc)
+apply (metis One_nat_def differentiableI dlo_simps(7))
 apply safe
 apply force
 apply (frule Maclaurin_lemma3, assumption+, safe)