# HG changeset patch
# User haftmann
# Date 1313796082 -7200
# Node ID 4b5b430eb00e878e9f7945cf02672e2035d2bd12
# Parent  d4decbd67703837bdfa14abbad62bf824c8a8f12# Parent  43b465f4c4805d357d7fce035c5a3c38fc32deb0
merged

diff -r 43b465f4c480 -r 4b5b430eb00e src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 20 01:21:22 2011 +0200
@@ -839,7 +839,8 @@
       cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
       + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
       (is "_ = ?SUM + ?rest / ?fact * ?pow")
-      using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`] by auto
+      using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
+      unfolding cos_coeff_def by auto
 
     have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
     also have "\<dots> = cos (t + n * pi)"  using cos_add by auto
@@ -951,7 +952,8 @@
       sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
       + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
       (is "_ = ?SUM + ?rest / ?fact * ?pow")
-      using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`] by auto
+      using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
+      unfolding sin_coeff_def by auto
 
     have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add left_distrib right_distrib by auto
     moreover
@@ -959,7 +961,7 @@
     hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
     ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le> - ?rest " by auto
 
-    have "0 < ?fact" by (rule real_of_nat_fact_gt_zero)
+    have "0 < ?fact" by (simp del: fact_Suc)
     have "0 < ?pow" using `0 < real x` by (rule zero_less_power)
 
     {
diff -r 43b465f4c480 -r 4b5b430eb00e src/HOL/Ln.thy
--- a/src/HOL/Ln.thy	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/HOL/Ln.thy	Sat Aug 20 01:21:22 2011 +0200
@@ -65,7 +65,7 @@
         apply (rule mult_right_mono)
         apply (subst inverse_eq_divide)
         apply simp
-        apply (rule inv_real_of_nat_fact_ge_zero)
+        apply (simp del: fact_Suc)
         done
       finally show ?thesis .
     qed
diff -r 43b465f4c480 -r 4b5b430eb00e src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/HOL/MacLaurin.thy	Sat Aug 20 01:21:22 2011 +0200
@@ -417,32 +417,33 @@
       cos (x + real (m) * pi / 2)"
 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
 
+lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
+  unfolding sin_coeff_def by simp (* TODO: move *)
+
 lemma Maclaurin_sin_expansion2:
      "\<exists>t. abs t \<le> abs x &
        sin x =
-       (\<Sum>m=0..<n. (if even m then 0
-                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
-                       x ^ m)
+       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = sin and n = n and x = x
         and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
 apply (simp (no_asm) add: sin_expansion_lemma)
-apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
+apply (force intro!: DERIV_intros)
+apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
+apply (cases n, simp, simp)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
 done
 
 lemma Maclaurin_sin_expansion:
      "\<exists>t. sin x =
-       (\<Sum>m=0..<n. (if even m then 0
-                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
-                       x ^ m)
+       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (insert Maclaurin_sin_expansion2 [of x n])
 apply (blast intro: elim:)
@@ -452,44 +453,44 @@
      "[| n > 0; 0 < x |] ==>
        \<exists>t. 0 < t & t < x &
        sin x =
-       (\<Sum>m=0..<n. (if even m then 0
-                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
-                       x ^ m)
+       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
       + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
 apply safe
 apply simp
 apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
 done
 
 lemma Maclaurin_sin_expansion4:
      "0 < x ==>
        \<exists>t. 0 < t & t \<le> x &
        sin x =
-       (\<Sum>m=0..<n. (if even m then 0
-                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
-                       x ^ m)
+       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
 apply safe
 apply simp
 apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
 done
 
 
 subsection{*Maclaurin Expansion for Cosine Function*}
 
+lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
+  unfolding cos_coeff_def by simp (* TODO: move *)
+
 lemma sumr_cos_zero_one [simp]:
- "(\<Sum>m=0..<(Suc n).
-     (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
+  "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
 by (induct "n", auto)
 
 lemma cos_expansion_lemma:
@@ -499,10 +500,7 @@
 lemma Maclaurin_cos_expansion:
      "\<exists>t. abs t \<le> abs x &
        cos x =
-       (\<Sum>m=0..<n. (if even m
-                       then -1 ^ (m div 2)/(real (fact m))
-                       else 0) *
-                       x ^ m)
+       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
 apply safe
@@ -515,17 +513,14 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
 done
 
 lemma Maclaurin_cos_expansion2:
      "[| 0 < x; n > 0 |] ==>
        \<exists>t. 0 < t & t < x &
        cos x =
-       (\<Sum>m=0..<n. (if even m
-                       then -1 ^ (m div 2)/(real (fact m))
-                       else 0) *
-                       x ^ m)
+       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
 apply safe
@@ -534,17 +529,14 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
 done
 
 lemma Maclaurin_minus_cos_expansion:
      "[| x < 0; n > 0 |] ==>
        \<exists>t. x < t & t < 0 &
        cos x =
-       (\<Sum>m=0..<n. (if even m
-                       then -1 ^ (m div 2)/(real (fact m))
-                       else 0) *
-                       x ^ m)
+       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
 apply safe
@@ -553,7 +545,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
 done
 
 (* ------------------------------------------------------------------------- *)
@@ -565,8 +557,8 @@
 by auto
 
 lemma Maclaurin_sin_bound:
-  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
-  x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
+  "abs(sin x - (\<Sum>m=0..<n. sin_coeff m * x ^ m))
+  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
 proof -
   have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
     by (rule_tac mult_right_mono,simp_all)
@@ -592,6 +584,7 @@
     apply (safe dest!: mod_eqD, simp_all)
     done
   show ?thesis
+    unfolding sin_coeff_def
     apply (subst t2)
     apply (rule sin_bound_lemma)
     apply (rule setsum_cong[OF refl])
diff -r 43b465f4c480 -r 4b5b430eb00e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/HOL/Transcendental.thy	Sat Aug 20 01:21:22 2011 +0200
@@ -618,23 +618,6 @@
 qed
 
 
-subsection{* Some properties of factorials *}
-
-lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
-by auto
-
-lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
-by auto
-
-lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
-by simp
-
-lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
-by (auto simp add: positive_imp_inverse_positive)
-
-lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
-by (auto intro: order_less_imp_le)
-
 subsection {* Derivability of power series *}
 
 lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
@@ -820,9 +803,8 @@
 
 subsection {* Exponential Function *}
 
-definition
-  exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
-  "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
+definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
+  "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
 
 lemma summable_exp_generic:
   fixes x :: "'a::{real_normed_algebra_1,banach}"
@@ -880,14 +862,10 @@
 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
 by (simp add: diffs_def)
 
-lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
-by (auto simp add: exp_def)
-
 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
-apply (simp add: exp_def)
-apply (subst lemma_exp_ext)
-apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)")
-apply (rule_tac [2] K = "of_real (1 + norm x)" in termdiffs)
+unfolding exp_def scaleR_conv_of_real
+apply (rule DERIV_cong)
+apply (rule termdiffs [where K="of_real (1 + norm x)"])
 apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
 apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
 apply (simp del: of_real_add)
@@ -1100,120 +1078,93 @@
 
 subsection {* Natural Logarithm *}
 
-definition
-  ln :: "real => real" where
+definition ln :: "real \<Rightarrow> real" where
   "ln x = (THE u. exp u = x)"
 
 lemma ln_exp [simp]: "ln (exp x) = x"
-by (simp add: ln_def)
+  by (simp add: ln_def)
 
 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
-by (auto dest: exp_total)
+  by (auto dest: exp_total)
 
 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
-apply (rule iffI)
-apply (erule subst, rule exp_gt_zero)
-apply (erule exp_ln)
-done
+  by (metis exp_gt_zero exp_ln)
 
 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
-by (erule subst, rule ln_exp)
+  by (erule subst, rule ln_exp)
 
 lemma ln_one [simp]: "ln 1 = 0"
-by (rule ln_unique, simp)
+  by (rule ln_unique, simp)
 
 lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y"
-by (rule ln_unique, simp add: exp_add)
+  by (rule ln_unique, simp add: exp_add)
 
 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
-by (rule ln_unique, simp add: exp_minus)
+  by (rule ln_unique, simp add: exp_minus)
 
 lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x - ln y"
-by (rule ln_unique, simp add: exp_diff)
+  by (rule ln_unique, simp add: exp_diff)
 
 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
-by (rule ln_unique, simp add: exp_real_of_nat_mult)
+  by (rule ln_unique, simp add: exp_real_of_nat_mult)
 
 lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
-by (subst exp_less_cancel_iff [symmetric], simp)
+  by (subst exp_less_cancel_iff [symmetric], simp)
 
 lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
-by (simp add: linorder_not_less [symmetric])
+  by (simp add: linorder_not_less [symmetric])
 
 lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
-by (simp add: order_eq_iff)
+  by (simp add: order_eq_iff)
 
 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
-apply (rule exp_le_cancel_iff [THEN iffD1])
-apply (simp add: exp_ge_add_one_self_aux)
-done
+  apply (rule exp_le_cancel_iff [THEN iffD1])
+  apply (simp add: exp_ge_add_one_self_aux)
+  done
 
 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
-by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
-
-lemma ln_ge_zero [simp]:
-  assumes x: "1 \<le> x" shows "0 \<le> ln x"
-proof -
-  have "0 < x" using x by arith
-  hence "exp 0 \<le> exp (ln x)"
-    by (simp add: x)
-  thus ?thesis by (simp only: exp_le_cancel_iff)
-qed
-
-lemma ln_ge_zero_imp_ge_one:
-  assumes ln: "0 \<le> ln x"
-      and x:  "0 < x"
-  shows "1 \<le> x"
-proof -
-  from ln have "ln 1 \<le> ln x" by simp
-  thus ?thesis by (simp add: x del: ln_one)
-qed
-
-lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
-by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
-
-lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
-by (insert ln_ge_zero_iff [of x], arith)
-
-lemma ln_gt_zero:
-  assumes x: "1 < x" shows "0 < ln x"
-proof -
-  have "0 < x" using x by arith
-  hence "exp 0 < exp (ln x)" by (simp add: x)
-  thus ?thesis  by (simp only: exp_less_cancel_iff)
-qed
-
-lemma ln_gt_zero_imp_gt_one:
-  assumes ln: "0 < ln x"
-      and x:  "0 < x"
-  shows "1 < x"
-proof -
-  from ln have "ln 1 < ln x" by simp
-  thus ?thesis by (simp add: x del: ln_one)
-qed
-
-lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
-by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
-
-lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
-by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
-
-lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
-by simp
+  by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
+
+lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
+  using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_ge_zero_imp_ge_one: "\<lbrakk>0 \<le> ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 \<le> x"
+  using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> (0 \<le> ln x) = (1 \<le> x)"
+  using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x < 0) = (x < 1)"
+  using ln_less_cancel_iff [of x 1] by simp
+
+lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
+  using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_gt_zero_imp_gt_one: "\<lbrakk>0 < ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x"
+  using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> (0 < ln x) = (1 < x)"
+  using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x = 0) = (x = 1)"
+  using ln_inj_iff [of x 1] by simp
+
+lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0"
+  by simp
 
 lemma exp_ln_eq: "exp u = x ==> ln x = u"
-by auto
+  by (rule ln_unique) (* TODO: delete *)
 
 lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
-apply (subgoal_tac "isCont ln (exp (ln x))", simp)
-apply (rule isCont_inverse_function [where f=exp], simp_all)
-done
+  apply (subgoal_tac "isCont ln (exp (ln x))", simp)
+  apply (rule isCont_inverse_function [where f=exp], simp_all)
+  done
 
 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
-apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
-apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
-apply (simp_all add: abs_if isCont_ln)
-done
+  apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
+  apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
+  apply (simp_all add: abs_if isCont_ln)
+  done
 
 lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
   by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
@@ -1253,60 +1204,30 @@
 
 subsection {* Sine and Cosine *}
 
-definition
-  sin_coeff :: "nat \<Rightarrow> real" where
+definition sin_coeff :: "nat \<Rightarrow> real" where
   "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
 
-definition
-  cos_coeff :: "nat \<Rightarrow> real" where
+definition cos_coeff :: "nat \<Rightarrow> real" where
   "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
 
-definition
-  sin :: "real => real" where
-  "sin x = (\<Sum>n. sin_coeff n * x ^ n)"
-
-definition
-  cos :: "real => real" where
-  "cos x = (\<Sum>n. cos_coeff n * x ^ n)"
+definition sin :: "real \<Rightarrow> real" where
+  "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
+
+definition cos :: "real \<Rightarrow> real" where
+  "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
 
 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
 unfolding sin_coeff_def
-apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
-apply (rule_tac [2] summable_exp)
-apply (rule_tac x = 0 in exI)
+apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
 done
 
 lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
 unfolding cos_coeff_def
-apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
-apply (rule_tac [2] summable_exp)
-apply (rule_tac x = 0 in exI)
+apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
 done
 
-lemma lemma_STAR_sin:
-     "(if even n then 0
-       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos:
-     "0 < n -->
-      -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos1:
-     "0 < n -->
-      (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos2:
-  "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n
-                         else 0) = 0"
-apply (induct "n")
-apply (case_tac [2] "n", auto)
-done
-
 lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
 unfolding sin_def by (rule summable_sin [THEN summable_sums])
 
@@ -1336,22 +1257,15 @@
 lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))"
 by (auto intro!: sums_unique sums_minus sin_converges)
 
-lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
-  by (auto simp add: sin_def)
-
-lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
-  by (auto simp add: cos_def)
-
 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
-apply (simp add: cos_def)
-apply (subst lemma_sin_ext)
+unfolding sin_def cos_def
 apply (auto simp add: sin_fdiffs2 [symmetric])
 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
 apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
 done
 
 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
-apply (subst lemma_cos_ext)
+unfolding cos_def
 apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
 apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
@@ -1378,196 +1292,122 @@
 lemma cos_zero [simp]: "cos 0 = 1"
 unfolding cos_def cos_coeff_def by (simp add: powser_zero)
 
-lemma DERIV_sin_sin_mult [simp]:
-     "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"
-by (rule DERIV_mult, auto)
-
-lemma DERIV_sin_sin_mult2 [simp]:
-     "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
-apply (cut_tac x = x in DERIV_sin_sin_mult)
-apply (auto simp add: mult_assoc)
-done
-
-lemma DERIV_sin_realpow2 [simp]:
-     "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
-
-lemma DERIV_sin_realpow2a [simp]:
-     "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2)
-
-lemma DERIV_cos_cos_mult [simp]:
-     "DERIV (%x. cos(x)*cos(x)) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
-by (rule DERIV_mult, auto)
-
-lemma DERIV_cos_cos_mult2 [simp]:
-     "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
-apply (cut_tac x = x in DERIV_cos_cos_mult)
-apply (auto simp add: mult_ac)
-done
-
-lemma DERIV_cos_realpow2 [simp]:
-     "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
-by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
-
-lemma DERIV_cos_realpow2a [simp]:
-     "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2)
-
 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
-by auto
-
-lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
-  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))"
-  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))"
-  by (auto intro!: DERIV_intros)
-
-lemma DERIV_sin_circle_all_zero [simp]:
-     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
-by (cut_tac DERIV_sin_circle_all, auto)
-
-lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
-apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all])
-apply (auto simp add: numeral_2_eq_2)
-done
-
-lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
-apply (subst add_commute)
-apply (rule sin_cos_squared_add)
-done
+  by (rule DERIV_cong) (* TODO: delete *)
+
+lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
+proof -
+  have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
+    by (auto intro!: DERIV_intros)
+  hence "(sin x)\<twosuperior> + (cos x)\<twosuperior> = (sin 0)\<twosuperior> + (cos 0)\<twosuperior>"
+    by (rule DERIV_isconst_all)
+  thus "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1" by simp
+qed
+
+lemma sin_cos_squared_add2 [simp]: "(cos x)\<twosuperior> + (sin x)\<twosuperior> = 1"
+  by (subst add_commute, rule sin_cos_squared_add)
 
 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
-apply (cut_tac x = x in sin_cos_squared_add2)
-apply (simp add: power2_eq_square)
-done
+  using sin_cos_squared_add2 [unfolded power2_eq_square] .
 
 lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
-apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
-apply simp
-done
+  unfolding eq_diff_eq by (rule sin_cos_squared_add)
 
 lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
-apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
-apply simp
-done
+  unfolding eq_diff_eq by (rule sin_cos_squared_add2)
 
 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
-by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
+  by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
 
 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
-apply (insert abs_sin_le_one [of x])
-apply (simp add: abs_le_iff del: abs_sin_le_one)
-done
+  using abs_sin_le_one [of x] unfolding abs_le_iff by simp
 
 lemma sin_le_one [simp]: "sin x \<le> 1"
-apply (insert abs_sin_le_one [of x])
-apply (simp add: abs_le_iff del: abs_sin_le_one)
-done
+  using abs_sin_le_one [of x] unfolding abs_le_iff by simp
 
 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
-by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
+  by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
 
 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
-apply (insert abs_cos_le_one [of x])
-apply (simp add: abs_le_iff del: abs_cos_le_one)
-done
+  using abs_cos_le_one [of x] unfolding abs_le_iff by simp
 
 lemma cos_le_one [simp]: "cos x \<le> 1"
-apply (insert abs_cos_le_one [of x])
-apply (simp add: abs_le_iff del: abs_cos_le_one)
-done
+  using abs_cos_le_one [of x] unfolding abs_le_iff by simp
 
 lemma DERIV_fun_pow: "DERIV g x :> m ==>
       DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
 unfolding One_nat_def
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
 apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
 apply (rule DERIV_pow, auto)
 done
 
 lemma DERIV_fun_exp:
      "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
 apply (rule_tac f = exp in DERIV_chain2)
 apply (rule DERIV_exp, auto)
 done
 
 lemma DERIV_fun_sin:
      "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
 apply (rule_tac f = sin in DERIV_chain2)
 apply (rule DERIV_sin, auto)
 done
 
 lemma DERIV_fun_cos:
      "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
 apply (rule_tac f = cos in DERIV_chain2)
 apply (rule DERIV_cos, auto)
 done
 
-(* 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"
-  by (auto intro!: DERIV_intros simp add: algebra_simps)
-
-lemma sin_cos_add [simp]:
+lemma sin_cos_add_lemma:
      "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
       (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
-apply (cut_tac y = 0 and x = x and y7 = y
-       in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
-apply (auto simp add: numeral_2_eq_2)
-done
+  (is "?f x = 0")
+proof -
+  have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
+    by (auto intro!: DERIV_intros simp add: algebra_simps)
+  hence "?f x = ?f 0"
+    by (rule DERIV_isconst_all)
+  thus ?thesis by simp
+qed
 
 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
-apply (cut_tac x = x and y = y in sin_cos_add)
-apply (simp del: sin_cos_add)
-done
+  using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
 
 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
-apply (cut_tac x = x and y = y in sin_cos_add)
-apply (simp del: sin_cos_add)
-done
-
-lemma lemma_DERIV_sin_cos_minus:
-    "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
-  by (auto intro!: DERIV_intros simp add: algebra_simps)
-
-
-lemma sin_cos_minus:
-    "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
-apply (cut_tac y = 0 and x = x
-       in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
-apply simp
-done
+  using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
+
+lemma sin_cos_minus_lemma:
+  "(sin(-x) + sin(x))\<twosuperior> + (cos(-x) - cos(x))\<twosuperior> = 0" (is "?f x = 0")
+proof -
+  have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
+    by (auto intro!: DERIV_intros simp add: algebra_simps)
+  hence "?f x = ?f 0"
+    by (rule DERIV_isconst_all)
+  thus ?thesis by simp
+qed
 
 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
-  using sin_cos_minus [where x=x] by simp
+  using sin_cos_minus_lemma [where x=x] by simp
 
 lemma cos_minus [simp]: "cos (-x) = cos(x)"
-  using sin_cos_minus [where x=x] by simp
+  using sin_cos_minus_lemma [where x=x] by simp
 
 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
-by (simp add: diff_minus sin_add)
+  by (simp add: diff_minus sin_add)
 
 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
-by (simp add: sin_diff mult_commute)
+  by (simp add: sin_diff mult_commute)
 
 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
-by (simp add: diff_minus cos_add)
+  by (simp add: diff_minus cos_add)
 
 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
-by (simp add: cos_diff mult_commute)
+  by (simp add: cos_diff mult_commute)
 
 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
   using sin_add [where x=x and y=x] by simp
@@ -1579,8 +1419,7 @@
 
 subsection {* The Constant Pi *}
 
-definition
-  pi :: "real" where
+definition pi :: "real" where
   "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
 
 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
@@ -1701,7 +1540,8 @@
 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
             del: fact_Suc)
 apply (rule real_mult_inverse_cancel2)
-apply (rule real_of_nat_fact_gt_zero)+
+apply (simp del: fact_Suc)
+apply (simp del: fact_Suc)
 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
 apply (subst fact_lemma)
 apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
@@ -2467,7 +2307,7 @@
 lemma DERIV_arcsin:
   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
 apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
-apply (rule lemma_DERIV_subst [OF DERIV_sin])
+apply (rule DERIV_cong [OF DERIV_sin])
 apply (simp add: cos_arcsin)
 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
 apply (rule power_strict_mono, simp, simp, simp)
@@ -2480,7 +2320,7 @@
 lemma DERIV_arccos:
   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<twosuperior>))"
 apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
-apply (rule lemma_DERIV_subst [OF DERIV_cos])
+apply (rule DERIV_cong [OF DERIV_cos])
 apply (simp add: sin_arccos)
 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
 apply (rule power_strict_mono, simp, simp, simp)
@@ -2492,7 +2332,7 @@
 
 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<twosuperior>)"
 apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
-apply (rule lemma_DERIV_subst [OF DERIV_tan])
+apply (rule DERIV_cong [OF DERIV_tan])
 apply (rule cos_arctan_not_zero)
 apply (simp add: power_inverse tan_sec [symmetric])
 apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp)
@@ -2581,8 +2421,8 @@
 lemma tan_60: "tan (pi / 3) = sqrt 3"
 unfolding tan_def by (simp add: sin_60 cos_60)
 
-lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
-  by (auto intro!: DERIV_intros)
+lemma DERIV_sin_add: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
+  by (auto intro!: DERIV_intros) (* TODO: delete *)
 
 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
 proof -
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -31,6 +31,9 @@
     that lack regular result information, will pick up parallel
     exceptions from the cumulative group context (as Par_Exn).
 
+  * Future task groups may be canceled: present and future group
+    members will be interrupted eventually.
+
   * Promised "passive" futures are fulfilled by external means.  There
     is no associated evaluation task, but other futures can depend on
     them via regular join operations.
@@ -38,31 +41,35 @@
 
 signature FUTURE =
 sig
-  val worker_task: unit -> Task_Queue.task option
-  val worker_group: unit -> Task_Queue.group option
-  val worker_subgroup: unit -> Task_Queue.group
+  type task = Task_Queue.task
+  type group = Task_Queue.group
+  val new_group: group option -> group
+  val worker_task: unit -> task option
+  val worker_group: unit -> group option
+  val worker_subgroup: unit -> group
   type 'a future
-  val task_of: 'a future -> Task_Queue.task
+  val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
   val get_finished: 'a future -> 'a
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
-  val cancel_group: Task_Queue.group -> unit
-  val cancel: 'a future -> unit
+  val cancel_group: group -> task list
+  val cancel: 'a future -> task list
   type fork_params =
-   {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
-    pri: int, interrupts: bool}
+    {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
   val forks: fork_params -> (unit -> 'a) list -> 'a future list
   val fork_pri: int -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val join: 'a future -> 'a
+  val join_tasks: task list -> unit
+  val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
   val map: ('a -> 'b) -> 'a future -> 'b future
   val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
-  val promise_group: Task_Queue.group -> 'a future
-  val promise: unit -> 'a future
+  val promise_group: group -> (unit -> unit) -> 'a future
+  val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
   val shutdown: unit -> unit
@@ -74,17 +81,22 @@
 
 (** future values **)
 
+type task = Task_Queue.task;
+type group = Task_Queue.group;
+val new_group = Task_Queue.new_group;
+
+
 (* identifiers *)
 
 local
-  val tag = Universal.tag () : Task_Queue.task option Universal.tag;
+  val tag = Universal.tag () : task option Universal.tag;
 in
   fun worker_task () = the_default NONE (Thread.getLocal tag);
   fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
 end;
 
 val worker_group = Option.map Task_Queue.group_of_task o worker_task;
-fun worker_subgroup () = Task_Queue.new_group (worker_group ());
+fun worker_subgroup () = new_group (worker_group ());
 
 fun worker_joining e =
   (case worker_task () of
@@ -103,7 +115,7 @@
 
 datatype 'a future = Future of
  {promised: bool,
-  task: Task_Queue.task,
+  task: task,
   result: 'a result};
 
 fun task_of (Future {task, ...}) = task;
@@ -157,7 +169,7 @@
 val queue = Unsynchronized.ref Task_Queue.empty;
 val next = Unsynchronized.ref 0;
 val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
-val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
+val canceled = Unsynchronized.ref ([]: group list);
 val do_shutdown = Unsynchronized.ref false;
 val max_workers = Unsynchronized.ref 0;
 val max_active = Unsynchronized.ref 0;
@@ -172,15 +184,6 @@
 
 (* cancellation primitives *)
 
-fun interruptible_task f x =
-  if Multithreading.available then
-    Multithreading.with_attributes
-      (if is_some (worker_task ())
-       then Multithreading.private_interrupts
-       else Multithreading.public_interrupts)
-      (fn _ => f x)
-  else interruptible f x;
-
 fun cancel_now group = (*requires SYNCHRONIZED*)
   Task_Queue.cancel (! queue) group;
 
@@ -189,6 +192,17 @@
   broadcast scheduler_event);
 
 
+fun interruptible_task f x =
+  (if Multithreading.available then
+    Multithreading.with_attributes
+      (if is_some (worker_task ())
+       then Multithreading.private_interrupts
+       else Multithreading.public_interrupts)
+      (fn _ => f x)
+   else interruptible f x)
+  before Multithreading.interrupted ();
+
+
 (* worker threads *)
 
 fun worker_exec (task, jobs) =
@@ -208,10 +222,10 @@
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
-        val _ = Exn.capture Multithreading.interrupted ();
+        val test = Exn.capture Multithreading.interrupted ();
         val _ =
-          if ok then ()
-          else if cancel_now group then ()
+          if ok andalso not (Exn.is_interrupt_exn test) then ()
+          else if null (cancel_now group) then ()
           else cancel_later group;
         val _ = broadcast work_finished;
         val _ = if maximal then () else signal work_available;
@@ -244,7 +258,7 @@
 fun worker_loop name =
   (case SYNCHRONIZED name (fn () => worker_next ()) of
     NONE => ()
-  | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
+  | SOME work => (worker_exec work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
@@ -345,7 +359,7 @@
       else
        (Multithreading.tracing 1 (fn () =>
           string_of_int (length (! canceled)) ^ " canceled groups");
-        Unsynchronized.change canceled (filter_out cancel_now);
+        Unsynchronized.change canceled (filter_out (null o cancel_now));
         broadcast_work ());
 
 
@@ -388,12 +402,15 @@
 
 (** futures **)
 
-(* cancellation *)
+(* cancel *)
 
-(*cancel: present and future group members will be interrupted eventually*)
-fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
- (if cancel_now group then () else cancel_later group;
-  signal work_available; scheduler_check ()));
+fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
+  let
+    val running = cancel_now group;
+    val _ =
+      if null running then ()
+      else (cancel_later group; signal work_available; scheduler_check ());
+  in running end);
 
 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
 
@@ -430,8 +447,7 @@
               Multithreading.with_attributes
                 (if interrupts
                  then Multithreading.private_interrupts else Multithreading.no_interrupts)
-                (fn _ => Position.setmp_thread_data pos e ()) before
-              Multithreading.interrupted ()) ()
+                (fn _ => Position.setmp_thread_data pos e ())) ()
           else Exn.interrupt_exn;
       in assign_result group result res end;
   in (result, job) end;
@@ -440,8 +456,7 @@
 (* fork *)
 
 type fork_params =
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
-  pri: int, interrupts: bool};
+  {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
 
 fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
   if null es then []
@@ -469,7 +484,7 @@
     end;
 
 fun fork_pri pri e =
-  singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
+  (singleton o forks) {name = "fork", group = NONE, deps = [], pri = pri, interrupts = true} e;
 
 fun fork e = fork_pri 0 e;
 
@@ -521,21 +536,30 @@
 fun join_result x = singleton join_results x;
 fun join x = Exn.release (join_result x);
 
+fun join_tasks [] = ()
+  | join_tasks tasks =
+      (singleton o forks)
+        {name = "join_tasks", group = SOME (new_group NONE),
+          deps = tasks, pri = 0, interrupts = false} I
+      |> join;
+
 
 (* fast-path versions -- bypassing task queue *)
 
-fun value (x: 'a) =
+fun value_result (res: 'a Exn.result) =
   let
     val task = Task_Queue.dummy_task ();
     val group = Task_Queue.group_of_task task;
     val result = Single_Assignment.var "value" : 'a result;
-    val _ = assign_result group result (Exn.Res x);
+    val _ = assign_result group result res;
   in Future {promised = false, task = task, result = result} end;
 
+fun value x = value_result (Exn.Res x);
+
 fun map_future f x =
   let
     val task = task_of x;
-    val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
+    val group = new_group (SOME (Task_Queue.group_of_task task));
     val (result, job) = future_job group true (fn () => f (join x));
 
     val extended = SYNCHRONIZED "extend" (fn () =>
@@ -545,32 +569,36 @@
   in
     if extended then Future {promised = false, task = task, result = result}
     else
-      singleton
-        (forks {name = "Future.map", group = SOME group, deps = [task],
-          pri = Task_Queue.pri_of_task task, interrupts = true})
+      (singleton o forks)
+        {name = "map_future", group = SOME group, deps = [task],
+          pri = Task_Queue.pri_of_task task, interrupts = true}
         (fn () => f (join x))
   end;
 
 fun cond_forks args es =
   if Multithreading.enabled () then forks args es
-  else map (fn e => value (e ())) es;
+  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
 
 
 (* promised futures -- fulfilled by external means *)
 
-fun promise_group group : 'a future =
+fun promise_group group abort : 'a future =
   let
     val result = Single_Assignment.var "promise" : 'a result;
-    fun abort () = assign_result group result Exn.interrupt_exn
+    fun assign () = assign_result group result Exn.interrupt_exn
       handle Fail _ => true
         | exn =>
-            if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise"
+            if Exn.is_interrupt exn
+            then raise Fail "Concurrent attempt to fulfill promise"
             else reraise exn;
+    fun job () =
+      Multithreading.with_attributes Multithreading.no_interrupts
+        (fn _ => assign () before abort ());
     val task = SYNCHRONIZED "enqueue_passive" (fn () =>
-      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
+      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
   in Future {promised = true, task = task, result = result} end;
 
-fun promise () = promise_group (worker_subgroup ());
+fun promise abort = promise_group (worker_subgroup ()) abort;
 
 fun fulfill_result (Future {promised, task, result}) res =
   if not promised then raise Fail "Not a promised future"
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -57,7 +57,7 @@
           val (expr, x) =
             Synchronized.change_result var
               (fn Expr e =>
-                    let val x = Future.promise ()
+                    let val x = Future.promise I
                     in ((SOME e, x), Result x) end
                 | Result x => ((NONE, x), Result x));
         in
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -22,7 +22,11 @@
 fun serial exn =
   (case get_exn_serial exn of
     SOME i => (i, exn)
-  | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
+  | NONE =>
+      let
+        val i = Library.serial ();
+        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
+      in (i, exn') end);
 
 val the_serial = the o get_exn_serial;
 
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -34,12 +34,13 @@
   then map (Exn.capture f) xs
   else
     let
-      val group = Task_Queue.new_group (Future.worker_group ());
+      val group = Future.new_group (Future.worker_group ());
       val futures =
         Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
           (map (fn x => fn () => f x) xs);
       val results = Future.join_results futures
-        handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+        handle exn =>
+          (if Exn.is_interrupt exn then ignore (Future.cancel_group group) else (); reraise exn);
     in results end;
 
 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -31,7 +31,7 @@
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int, passive: int}
-  val cancel: queue -> group -> bool
+  val cancel: queue -> group -> task list
   val cancel_all: queue -> group list
   val finish: task -> queue -> bool * queue
   val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
@@ -248,10 +248,12 @@
   let
     val _ = cancel_group group Exn.Interrupt;
     val running =
-      Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
+      Tasks.fold (fn (task, _) =>
+          (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
         (get_tasks groups (group_id group)) [];
-    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
-  in null running end;
+    val threads = fold (insert Thread.equal o #2) running [];
+    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+  in map #1 running end;
 
 fun cancel_all (Queue {jobs, ...}) =
   let
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/General/markup.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -119,6 +119,7 @@
   val badN: string val bad: T
   val functionN: string
   val invoke_scala: string -> string -> Properties.T
+  val cancel_scala: string -> Properties.T
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -377,6 +378,7 @@
 val functionN = "function"
 
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
+fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
 
 
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/General/markup.scala	Sat Aug 20 01:21:22 2011 +0200
@@ -283,6 +283,16 @@
       }
   }
 
+  val CANCEL_SCALA = "cancel_scala"
+  object Cancel_Scala
+  {
+    def unapply(props: Properties.T): Option[String] =
+      props match {
+        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
+        case _ => None
+      }
+  }
+
 
   /* system data */
 
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -119,7 +119,7 @@
   else f x;
 
 fun controlled_execution f x =
-  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
+  (f |> debugging |> Future.interruptible_task) x;
 
 fun toplevel_error output_exn f x = f x
   handle exn =>
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -419,6 +419,14 @@
 
 (* theory transitions *)
 
+val global_theory_group =
+  Sign.new_group #>
+  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+
+val local_theory_group =
+  Local_Theory.new_group #>
+  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+
 fun generic_theory f = transaction (fn _ =>
   (fn Theory (gthy, _) => Theory (f gthy, NONE)
     | _ => raise UNDEF));
@@ -426,8 +434,7 @@
 fun theory' f = transaction (fn int =>
   (fn Theory (Context.Theory thy, _) =>
       let val thy' = thy
-        |> Sign.new_group
-        |> Theory.checkpoint
+        |> global_theory_group
         |> f int
         |> Sign.reset_group;
       in Theory (Context.Theory thy', NONE) end
@@ -454,7 +461,7 @@
         let
           val finish = loc_finish loc gthy;
           val lthy' = loc_begin loc gthy
-            |> Local_Theory.new_group
+            |> local_theory_group
             |> f int
             |> Local_Theory.reset_group;
         in Theory (finish lthy', SOME lthy') end
@@ -506,13 +513,13 @@
 in
 
 fun local_theory_to_proof' loc f = begin_proof
-  (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
+  (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy)))
   (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
 
 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
 
 fun theory_to_proof f = begin_proof
-  (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
+  (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))
   (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
 
 end;
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -24,7 +24,7 @@
   type state
   val init_state: state
   val join_commands: state -> unit
-  val cancel_execution: state -> unit -> unit
+  val cancel_execution: state -> Future.task list
   val define_command: command_id -> string -> state -> state
   val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
@@ -164,7 +164,7 @@
  {versions: version Inttab.table,  (*version_id -> document content*)
   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
   execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
-  execution: unit future list}  (*global execution process*)
+  execution: Future.group}  (*global execution process*)
 with
 
 fun make_state (versions, commands, execs, execution) =
@@ -177,7 +177,7 @@
   make_state (Inttab.make [(no_id, empty_version)],
     Inttab.make [(no_id, Future.value Toplevel.empty)],
     Inttab.make [(no_id, empty_exec)],
-    []);
+    Future.new_group NONE);
 
 
 (* document versions *)
@@ -200,9 +200,10 @@
   map_state (fn (versions, commands, execs, execution) =>
     let
       val id_string = print_id id;
-      val tr = Future.fork_pri 2 (fn () =>
-        Position.setmp_thread_data (Position.id_only id_string)
-          (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+      val tr =
+        Future.fork_pri 2 (fn () =>
+          Position.setmp_thread_data (Position.id_only id_string)
+            (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
       val commands' =
         Inttab.update_new (id, tr) commands
           handle Inttab.DUP dup => err_dup "command" dup;
@@ -233,9 +234,7 @@
 
 (* document execution *)
 
-fun cancel_execution (State {execution, ...}) =
-  (List.app Future.cancel execution;
-    fn () => ignore (Future.join_results execution));
+fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
 
 end;
 
@@ -253,13 +252,13 @@
   | NONE => ());
 
 fun async_state tr st =
-  ignore
-    (singleton
-      (Future.forks {name = "Document.async_state",
-        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
-      (fn () =>
-        Toplevel.setmp_thread_position tr
-          (fn () => Toplevel.print_state false st) ()));
+  (singleton o Future.forks)
+    {name = "Document.async_state", group = SOME (Future.new_group NONE),
+      deps = [], pri = 0, interrupts = true}
+    (fn () =>
+      Toplevel.setmp_thread_position tr
+        (fn () => Toplevel.print_state false st) ())
+  |> ignore;
 
 fun run int tr st =
   (case Toplevel.transition int tr st of
@@ -355,9 +354,9 @@
                 fun get_command id =
                   (id, the_command state id |> Future.map (Toplevel.modify_init init));
               in
-                singleton
-                  (Future.forks {name = "Document.edit", group = NONE,
-                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
+                (singleton o Future.forks)
+                  {name = "Document.edit", group = NONE,
+                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
                   (fn () =>
                     let
                       val prev_exec =
@@ -393,17 +392,16 @@
       fun force_exec NONE = ()
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
-      val execution' =
+      val execution = Future.new_group NONE;
+      val _ =
         nodes_of version |> Graph.schedule
           (fn deps => fn (name, node) =>
-            singleton
-              (Future.forks
-                {name = "theory:" ^ name, group = NONE,
-                  deps = map (Future.task_of o #2) deps,
-                  pri = 1, interrupts = true})
+            (singleton o Future.forks)
+              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
+                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
               (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
 
-    in (versions, commands, execs, execution') end);
+    in (versions, commands, execs, execution) end);
 
 
 
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -30,9 +30,9 @@
                   fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
             end;
 
-      val await_cancellation = Document.cancel_execution state;
+      val running = Document.cancel_execution state;
       val (updates, state') = Document.edit old_id new_id edits state;
-      val _ = await_cancellation ();
+      val _ = Future.join_tasks running;
       val _ = Document.join_commands state';
       val _ =
         Output.status (Markup.markup (Markup.assign new_id)
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/System/invoke_scala.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -33,7 +33,8 @@
 fun promise_method name arg =
   let
     val id = new_id ();
-    val promise = Future.promise () : string future;
+    fun abort () = Output.raw_message (Markup.cancel_scala id) "";
+    val promise = Future.promise abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
     val _ = Output.raw_message (Markup.invoke_scala name id) arg;
   in promise end;
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 20 01:21:22 2011 +0200
@@ -275,6 +275,8 @@
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
+        case Markup.Cancel_Scala(id) =>
+          System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -194,11 +194,9 @@
   Graph.schedule (fn deps => fn (name, task) =>
     (case task of
       Task (parents, body) =>
-        singleton
-          (Future.forks
-            {name = "theory:" ^ name, group = NONE,
-              deps = map (Future.task_of o #2) deps,
-              pri = 0, interrupts = true})
+        (singleton o Future.forks)
+          {name = "theory:" ^ name, group = NONE,
+            deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
           (fn () =>
             (case filter (not o can Future.join o #2) deps of
               [] => body (map (#1 o Future.join) (task_parents deps parents))
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/global_theory.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -10,6 +10,8 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
+  val begin_recent_proofs: theory -> theory
+  val join_recent_proofs: theory -> unit
   val join_proofs: theory -> unit
   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
@@ -49,10 +51,10 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * thm list;
-  val empty = (Facts.empty, []);
-  fun extend (facts, _) = (facts, []);
-  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+  type T = Facts.T * (thm list * thm list);
+  val empty = (Facts.empty, ([], []));
+  fun extend (facts, _) = (facts, ([], []));
+  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
 );
 
 
@@ -68,10 +70,11 @@
 
 (* proofs *)
 
-fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
+fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (append thms))) thy, thms);
 
-fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
-
+val begin_recent_proofs = Data.map (apsnd (fn (_, thms) => ([], thms)));
+val join_recent_proofs = Thm.join_proofs o rev o #1 o #2 o Data.get;
+val join_proofs = Thm.join_proofs o rev o #2 o #2 o Data.get;
 
 
 (** retrieve theorems **)
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/goal.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -124,8 +124,8 @@
     let
       val _ = forked 1;
       val future =
-        singleton
-          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
+        (singleton o Future.forks)
+          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
           (fn () =>
             Exn.release
               (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -37,11 +37,11 @@
 
   type oracle = string * term
   type pthm = serial * (string * term * proof_body future)
+  val join_body: proof_body -> unit
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
-  val join_bodies: proof_body list -> unit
   val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
@@ -171,6 +171,10 @@
 type oracle = string * term;
 type pthm = serial * (string * term * proof_body future);
 
+fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
+fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
+fun join_body (PBody {thms, ...}) = join_thms thms;
+
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
 
@@ -195,18 +199,15 @@
 fun fold_body_thms f =
   let
     fun app (PBody {thms, ...}) =
-     (Future.join_results (map (#3 o #2) thms);
-      thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+      tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
           let
             val body' = Future.join body;
             val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
-          in (f (name, prop, body') x', seen') end));
+          in (f (name, prop, body') x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
-fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
-
 fun status_of bodies =
   let
     fun status (PBody {oracles, thms, ...}) x =
@@ -242,14 +243,13 @@
 val all_oracles_of =
   let
     fun collect (PBody {oracles, thms, ...}) =
-     (Future.join_results (map (#3 o #2) thms);
-      thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+      tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
           let
             val body' = Future.join body;
             val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
-          in (merge_oracles oracles x', seen') end));
+          in (merge_oracles oracles x', seen') end);
   in fn body => #1 (collect body ([], Inttab.empty)) end;
 
 fun approximate_proof_body prf =
@@ -1396,16 +1396,17 @@
       | fill _ = NONE;
     val (rules, procs) = get_data thy;
     val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
+    val _ = join_thms thms;
   in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
 fun fulfill_proof_future _ [] postproc body =
       if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
       else Future.map postproc body
   | fulfill_proof_future thy promises postproc body =
-      singleton
-        (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
-            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
-            interrupts = true})
+      (singleton o Future.forks)
+        {name = "Proofterm.fulfill_proof_future", group = NONE,
+          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+          interrupts = true}
         (fn () =>
           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
 
@@ -1461,10 +1462,9 @@
       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
       else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
       else
-        singleton
-          (Future.forks
-            {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
-              interrupts = true})
+        (singleton o Future.forks)
+          {name = "Proofterm.prepare_thm_proof", group = NONE,
+            deps = [], pri = ~1, interrupts = true}
           (make_body0 o full_proof0);
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
diff -r 43b465f4c480 -r 4b5b430eb00e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/thm.ML	Sat Aug 20 01:21:22 2011 +0200
@@ -517,9 +517,9 @@
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
 and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
 
-val join_proofs = Proofterm.join_bodies o map fulfill_body;
+fun join_proofs thms = ignore (map fulfill_body thms);
 
-fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
+fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
 val proof_of = Proofterm.proof_of o proof_body_of;
 
 
diff -r 43b465f4c480 -r 4b5b430eb00e src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sat Aug 20 01:21:22 2011 +0200
@@ -21,7 +21,6 @@
   extends Dockable(view: View, position: String)
 {
   private val text_area = new TextArea
-  text_area.editable = false
   set_content(new ScrollPane(text_area))
 
 
diff -r 43b465f4c480 -r 4b5b430eb00e src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Aug 20 01:21:22 2011 +0200
@@ -28,7 +28,6 @@
   readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
 
   private val syslog = new TextArea(Isabelle.session.syslog())
-  syslog.editable = false
 
   private val tabs = new TabbedPane {
     pages += new TabbedPane.Page("README", Component.wrap(readme))