# HG changeset patch
# User haftmann
# Date 1246392220 -7200
# Node ID bf6207c7444874eae7cec682d590642ca6084f71
# Parent  905a27100f556ee95fa1b495a3782769e2b7b32f# Parent  7d8a89390cbf8d1c30163162c953fee3a4b23f3d
merged

diff -r 7d8a89390cbf -r bf6207c74448 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Tue Jun 30 19:45:52 2009 +0200
+++ b/Admin/isatest/isatest-makedist	Tue Jun 30 22:03:40 2009 +0200
@@ -106,7 +106,7 @@
 sleep 15
 $SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
+$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4"
 sleep 15
 $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
 sleep 15
diff -r 7d8a89390cbf -r bf6207c74448 Admin/isatest/settings/mac-poly64-M4
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/mac-poly64-M4	Tue Jun 30 22:03:40 2009 +0200
@@ -0,0 +1,28 @@
+# -*- shell-script -*- :mode=shellscript:
+
+  POLYML_HOME="/home/polyml/polyml-svn"
+  ML_SYSTEM="polyml-experimental"
+  ML_PLATFORM="x86_64-darwin"
+  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+  ML_OPTIONS="--mutable 2000 --immutable 2000"
+
+
+ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
+
+# Where to look for isabelle tools (multiple dirs separated by ':').
+ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
+
+# Location for temporary files (should be on a local file system).
+ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+
+
+# Heap input locations. ML system identifier is included in lookup.
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+
+# Heap output location. ML system identifier is appended automatically later on.
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
+
+ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
+
+HOL_USEDIR_OPTIONS="-p 2 -Q false"
diff -r 7d8a89390cbf -r bf6207c74448 NEWS
--- a/NEWS	Tue Jun 30 19:45:52 2009 +0200
+++ b/NEWS	Tue Jun 30 22:03:40 2009 +0200
@@ -75,6 +75,14 @@
 * "approximate" supports now arithmetic expressions as boundaries of intervals and implements
 interval splitting and taylor series expansion.
 
+* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in DERIV_intros
+assumes composition with an additional function and matches a variable to the
+derivative, which has to be solved by the simplifier. Hence
+(auto intro!: DERIV_intros) computes the derivative of most elementary terms.
+
+* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by:
+(auto intro!: DERIV_intros)
+INCOMPATIBILITY.
 
 *** ML ***
 
diff -r 7d8a89390cbf -r bf6207c74448 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 30 22:03:40 2009 +0200
@@ -2670,11 +2670,6 @@
 "DERIV_floatarith x (Num f)           = Num 0" |
 "DERIV_floatarith x (Atom n)          = (if x = n then Num 1 else Num 0)"
 
-lemma DERIV_chain'': "\<lbrakk>DERIV g (f x) :> E ; DERIV f x :> D; x' = E * D \<rbrakk> \<Longrightarrow>
-  DERIV (\<lambda>x. g (f x)) x :> x'" using DERIV_chain' by auto
-
-lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = X' \<rbrakk> \<Longrightarrow> DERIV f x :> X'" by simp
-
 lemma DERIV_floatarith:
   assumes "n < length vs"
   assumes isDERIV: "isDERIV n f (vs[n := x])"
@@ -2682,31 +2677,20 @@
                interpret_floatarith (DERIV_floatarith n f) (vs[n := x])"
    (is "DERIV (?i f) x :> _")
 using isDERIV proof (induct f arbitrary: x)
-  case (Add a b) thus ?case by (auto intro: DERIV_add)
-next case (Mult a b) thus ?case by (auto intro!: DERIV_mult[THEN DERIV_cong])
-next case (Minus a) thus ?case by (auto intro!: DERIV_minus[THEN DERIV_cong])
-next case (Inverse a) thus ?case
-    by (auto intro!: DERIV_inverse_fun[THEN DERIV_cong] DERIV_inverse[THEN DERIV_cong]
+     case (Inverse a) thus ?case
+    by (auto intro!: DERIV_intros
              simp add: algebra_simps power2_eq_square)
 next case (Cos a) thus ?case
-  by (auto intro!: DERIV_chain''[of cos "?i a"]
-                   DERIV_cos[THEN DERIV_cong]
+  by (auto intro!: DERIV_intros
            simp del: interpret_floatarith.simps(5)
            simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
-next case (Arctan a) thus ?case
-  by (auto intro!: DERIV_chain''[of arctan "?i a"] DERIV_arctan[THEN DERIV_cong])
-next case (Exp a) thus ?case
-  by (auto intro!: DERIV_chain''[of exp "?i a"] DERIV_exp[THEN DERIV_cong])
 next case (Power a n) thus ?case
-  by (cases n, auto intro!: DERIV_power_Suc[THEN DERIV_cong]
+  by (cases n, auto intro!: DERIV_intros
                     simp del: power_Suc simp add: real_eq_of_nat)
-next case (Sqrt a) thus ?case
-    by (auto intro!: DERIV_chain''[of sqrt "?i a"] DERIV_real_sqrt[THEN DERIV_cong])
 next case (Ln a) thus ?case
-    by (auto intro!: DERIV_chain''[of ln "?i a"] DERIV_ln[THEN DERIV_cong]
-                     simp add: divide_inverse)
+    by (auto intro!: DERIV_intros simp add: divide_inverse)
 next case (Atom i) thus ?case using `n < length vs` by auto
-qed auto
+qed (auto intro!: DERIV_intros)
 
 declare approx.simps[simp del]
 
diff -r 7d8a89390cbf -r bf6207c74448 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Deriv.thy	Tue Jun 30 22:03:40 2009 +0200
@@ -115,12 +115,16 @@
 
 text{*Differentiation of finite sum*}
 
+lemma DERIV_setsum:
+  assumes "finite S"
+  and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
+  shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
+  using assms by induct (auto intro!: DERIV_add)
+
 lemma DERIV_sumr [rule_format (no_asm)]:
      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
       --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
-apply (induct "n")
-apply (auto intro: DERIV_add)
-done
+  by (auto intro: DERIV_setsum)
 
 text{*Alternative definition for differentiability*}
 
@@ -216,7 +220,6 @@
   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
 
-
 text {* Caratheodory formulation of derivative at a point *}
 
 lemma CARAT_DERIV:
@@ -308,6 +311,30 @@
 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
 by auto
 
+text {* DERIV_intros *}
+
+ML{*
+structure DerivIntros =
+  NamedThmsFun(val name = "DERIV_intros"
+               val description = "DERIV introduction rules");
+*}
+setup DerivIntros.setup
+
+lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
+  by simp
+
+declare
+  DERIV_const[THEN DERIV_cong, DERIV_intros]
+  DERIV_ident[THEN DERIV_cong, DERIV_intros]
+  DERIV_add[THEN DERIV_cong, DERIV_intros]
+  DERIV_minus[THEN DERIV_cong, DERIV_intros]
+  DERIV_mult[THEN DERIV_cong, DERIV_intros]
+  DERIV_diff[THEN DERIV_cong, DERIV_intros]
+  DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
+  DERIV_divide[THEN DERIV_cong, DERIV_intros]
+  DERIV_power[where 'a=real, THEN DERIV_cong,
+              unfolded real_of_nat_def[symmetric], DERIV_intros]
+  DERIV_setsum[THEN DERIV_cong, DERIV_intros]
 
 subsection {* Differentiability predicate *}
 
diff -r 7d8a89390cbf -r bf6207c74448 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 22:03:40 2009 +0200
@@ -85,13 +85,7 @@
 by (rule lemma_DERIV_subst, rule DERIV_add, auto)
 
 lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
-apply (induct p)
-apply simp
-apply (simp add: pderiv_pCons)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+
-apply simp
-done
+  by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
 
 text{* Consequences of the derivative theorem above*}
 
diff -r 7d8a89390cbf -r bf6207c74448 src/HOL/Ln.thy
--- a/src/HOL/Ln.thy	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Ln.thy	Tue Jun 30 22:03:40 2009 +0200
@@ -343,43 +343,7 @@
 done
 
 lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
-  apply (unfold deriv_def, unfold LIM_eq, clarsimp)
-  apply (rule exI)
-  apply (rule conjI)
-  prefer 2
-  apply clarsimp
-  apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) = 
-      (ln (1 + xa / x) - xa / x) / xa")
-  apply (erule ssubst)
-  apply (subst abs_divide)
-  apply (rule mult_imp_div_pos_less)
-  apply force
-  apply (rule order_le_less_trans)
-  apply (rule abs_ln_one_plus_x_minus_x_bound)
-  apply (subst abs_divide)
-  apply (subst abs_of_pos, assumption)
-  apply (erule mult_imp_div_pos_le)
-  apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
-  apply force
-  apply assumption
-  apply (simp add: power2_eq_square mult_compare_simps)
-  apply (rule mult_imp_div_pos_less)
-  apply (rule mult_pos_pos, assumption, assumption)
-  apply (subgoal_tac "xa * xa = abs xa * abs xa")
-  apply (erule ssubst)
-  apply (subgoal_tac "abs xa * (abs xa * 2) < abs xa * (r * (x * x))")
-  apply (simp only: mult_ac)
-  apply (rule mult_strict_left_mono)
-  apply (erule conjE, assumption)
-  apply force
-  apply simp
-  apply (subst ln_div [THEN sym])
-  apply arith
-  apply (auto simp add: algebra_simps add_frac_eq frac_eq_eq 
-    add_divide_distrib power2_eq_square)
-  apply (rule mult_pos_pos, assumption)+
-  apply assumption
-done
+  by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
 
 lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
 proof -
diff -r 7d8a89390cbf -r bf6207c74448 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/MacLaurin.thy	Tue Jun 30 22:03:40 2009 +0200
@@ -27,36 +27,6 @@
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
 by arith
 
-text{*A crude tactic to differentiate by proof.*}
-
-lemmas deriv_rulesI =
-  DERIV_ident DERIV_const DERIV_cos DERIV_cmult
-  DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
-  DERIV_add DERIV_diff DERIV_mult DERIV_minus
-  DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
-  DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
-  DERIV_ident DERIV_const DERIV_cos
-
-ML
-{*
-local
-exception DERIV_name;
-fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
-|   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
-|   get_fun_name _ = raise DERIV_name;
-
-in
-
-fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
-  resolve_tac @{thms deriv_rulesI} i ORELSE
-    ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
-                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
-
-fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
-
-end
-*}
-
 lemma Maclaurin_lemma2:
   assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   assumes n: "n = Suc k"
@@ -91,13 +61,12 @@
  apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
  apply (rule DERIV_cmult)
  apply (rule lemma_DERIV_subst)
-  apply (best intro: DERIV_chain2 intro!: DERIV_intros)
+  apply (best intro!: DERIV_intros)
  apply (subst fact_Suc)
  apply (subst real_of_nat_mult)
  apply (simp add: mult_ac)
 done
 
-
 lemma Maclaurin:
   assumes h: "0 < h"
   assumes n: "0 < n"
@@ -565,9 +534,7 @@
     apply (clarify)
     apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
     apply (cut_tac m=m in mod_exhaust_less_4)
-    apply (safe, simp_all)
-    apply (rule DERIV_minus, simp)
-    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
+    apply (safe, auto intro!: DERIV_intros)
     done
   from Maclaurin_all_le [OF diff_0 DERIV_diff]
   obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
diff -r 7d8a89390cbf -r bf6207c74448 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/NthRoot.thy	Tue Jun 30 22:03:40 2009 +0200
@@ -372,6 +372,41 @@
     using odd_pos [OF n] by (rule isCont_real_root)
 qed
 
+lemma DERIV_even_real_root:
+  assumes n: "0 < n" and "even n"
+  assumes x: "x < 0"
+  shows "DERIV (root n) x :> inverse (- real n * root n x ^ (n - Suc 0))"
+proof (rule DERIV_inverse_function)
+  show "x - 1 < x" by simp
+  show "x < 0" using x .
+next
+  show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
+  proof (rule allI, rule impI, erule conjE)
+    fix y assume "x - 1 < y" and "y < 0"
+    hence "root n (-y) ^ n = -y" using `0 < n` by simp
+    with real_root_minus[OF `0 < n`] and `even n`
+    show "- (root n y ^ n) = y" by simp
+  qed
+next
+  show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
+    by  (auto intro!: DERIV_intros)
+  show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
+    using n x by simp
+  show "isCont (root n) x"
+    using n by (rule isCont_real_root)
+qed
+
+lemma DERIV_real_root_generic:
+  assumes "0 < n" and "x \<noteq> 0"
+  and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+  and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
+  and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+  shows "DERIV (root n) x :> D"
+using assms by (cases "even n", cases "0 < x",
+  auto intro: DERIV_real_root[THEN DERIV_cong]
+              DERIV_odd_real_root[THEN DERIV_cong]
+              DERIV_even_real_root[THEN DERIV_cong])
+
 subsection {* Square Root *}
 
 definition
@@ -456,9 +491,21 @@
 lemma isCont_real_sqrt: "isCont sqrt x"
 unfolding sqrt_def by (rule isCont_real_root [OF pos2])
 
+lemma DERIV_real_sqrt_generic:
+  assumes "x \<noteq> 0"
+  assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
+  assumes "x < 0 \<Longrightarrow> D = - inverse (sqrt x) / 2"
+  shows "DERIV sqrt x :> D"
+  using assms unfolding sqrt_def
+  by (auto intro!: DERIV_real_root_generic)
+
 lemma DERIV_real_sqrt:
   "0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2"
-unfolding sqrt_def by (rule DERIV_real_root [OF pos2, simplified])
+  using DERIV_real_sqrt_generic by simp
+
+declare
+  DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
 
 lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
 apply auto
diff -r 7d8a89390cbf -r bf6207c74448 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Transcendental.thy	Tue Jun 30 22:03:40 2009 +0200
@@ -784,9 +784,8 @@
 	  also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
 	  finally show ?thesis .
 	qed }
-      { fix n
-	from DERIV_pow[of "Suc n" x0, THEN DERIV_cmult[where c="f n"]]
-	show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" unfolding real_mult_assoc by auto }
+      { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
+	  by (auto intro!: DERIV_intros simp del: power_Suc) }
       { fix x assume "x \<in> {-R' <..< R'}" hence "R' \<in> {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto
 	have "summable (\<lambda> n. f n * x^n)"
 	proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI)
@@ -1362,6 +1361,12 @@
 by (rule DERIV_cos [THEN DERIV_isCont])
 
 
+declare
+  DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
 subsection {* Properties of Sine and Cosine *}
 
 lemma sin_zero [simp]: "sin 0 = 0"
@@ -1410,24 +1415,17 @@
 by auto
 
 lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_realpow2a, auto)
-done
+  by (auto intro!: DERIV_intros)
 
 (* most useful *)
 lemma DERIV_cos_cos_mult3 [simp]:
      "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_cos_mult2, auto)
-done
+  by (auto intro!: DERIV_intros)
 
 lemma DERIV_sin_circle_all: 
      "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>  
              (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
-apply (simp only: diff_minus, safe)
-apply (rule DERIV_add) 
-apply (auto simp add: numeral_2_eq_2)
-done
+  by (auto intro!: DERIV_intros)
 
 lemma DERIV_sin_circle_all_zero [simp]:
      "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
@@ -1513,22 +1511,12 @@
 apply (rule DERIV_cos, auto)
 done
 
-lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
-                    DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
-                    DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
-                    DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
-                    DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
-
 (* lemma *)
 lemma lemma_DERIV_sin_cos_add:
      "\<forall>x.  
          DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
                (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2) 
-  --{*replaces the old @{text DERIV_tac}*}
-apply (auto simp add: algebra_simps)
-done
+  by (auto intro!: DERIV_intros simp add: algebra_simps)
 
 lemma sin_cos_add [simp]:
      "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
@@ -1550,10 +1538,8 @@
 
 lemma lemma_DERIV_sin_cos_minus:
     "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
-apply (simp add: algebra_simps)
-done
+  by (auto intro!: DERIV_intros simp add: algebra_simps)
+
 
 lemma sin_cos_minus: 
     "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
@@ -1722,7 +1708,7 @@
 apply (assumption, rule_tac y=y in order_less_le_trans, simp_all) 
 apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) 
 done
-    
+
 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
 by (simp add: pi_def)
 
@@ -2121,10 +2107,7 @@
 
 lemma lemma_DERIV_tan:
      "cos x \<noteq> 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\<twosuperior>)"
-apply (rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2) 
-apply (auto simp add: divide_inverse numeral_2_eq_2)
-done
+  by (auto intro!: DERIV_intros simp add: field_simps numeral_2_eq_2)
 
 lemma DERIV_tan [simp]: "cos x \<noteq> 0 ==> DERIV tan x :> inverse((cos x)\<twosuperior>)"
 by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
@@ -2500,6 +2483,11 @@
 apply (simp, simp, simp, rule isCont_arctan)
 done
 
+declare
+  DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
 subsection {* More Theorems about Sin and Cos *}
 
 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
@@ -2589,11 +2577,7 @@
 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
 
 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = sin and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+  by (auto intro!: DERIV_intros)
 
 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
 proof -
@@ -2634,11 +2618,7 @@
 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
 
 lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = cos and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+  by (auto intro!: DERIV_intros)
 
 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
 by (auto simp add: sin_zero_iff even_mult_two_ex)
diff -r 7d8a89390cbf -r bf6207c74448 src/Pure/General/swing.scala
--- a/src/Pure/General/swing.scala	Tue Jun 30 19:45:52 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-/*  Title:      Pure/General/swing.scala
-    Author:     Makarius
-
-Swing utilities.
-*/
-
-package isabelle
-
-import javax.swing.SwingUtilities
-
-object Swing
-{
-  def now[A](body: => A): A = {
-    var result: Option[A] = None
-    if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
-    else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
-    result.get
-  }
-
-  def later(body: => Unit) {
-    if (SwingUtilities.isEventDispatchThread) body
-    else SwingUtilities.invokeLater(new Runnable { def run = body })
-  }
-}
diff -r 7d8a89390cbf -r bf6207c74448 src/Pure/General/swing_thread.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/swing_thread.scala	Tue Jun 30 22:03:40 2009 +0200
@@ -0,0 +1,24 @@
+/*  Title:      Pure/General/swing_thread.scala
+    Author:     Makarius
+
+Evaluation within the AWT/Swing thread.
+*/
+
+package isabelle
+
+import javax.swing.SwingUtilities
+
+object Swing_Thread
+{
+  def now[A](body: => A): A = {
+    var result: Option[A] = None
+    if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
+    else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
+    result.get
+  }
+
+  def later(body: => Unit) {
+    if (SwingUtilities.isEventDispatchThread) body
+    else SwingUtilities.invokeLater(new Runnable { def run = body })
+  }
+}
diff -r 7d8a89390cbf -r bf6207c74448 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/Pure/IsaMakefile	Tue Jun 30 22:03:40 2009 +0200
@@ -118,7 +118,7 @@
 ## Scala material
 
 SCALA_FILES = General/event_bus.scala General/markup.scala		\
-  General/position.scala General/scan.scala General/swing.scala		\
+  General/position.scala General/scan.scala General/swing_thread.scala	\
   General/symbol.scala General/xml.scala General/yxml.scala		\
   Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
   System/cygwin.scala System/gui_setup.scala				\
diff -r 7d8a89390cbf -r bf6207c74448 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Tue Jun 30 19:45:52 2009 +0200
+++ b/src/Pure/System/gui_setup.scala	Tue Jun 30 22:03:40 2009 +0200
@@ -16,7 +16,7 @@
 {
   def main(args: Array[String]) =
   {
-    Swing.later {
+    Swing_Thread.later {
       UIManager.setLookAndFeel(Platform.look_and_feel)
       top.pack()
       top.visible = true