merged

--- a/.hgignore	Wed Jun 17 10:07:25 2009 +0200
+++ b/.hgignore	Wed Jun 17 10:08:06 2009 +0200
@@ -8,6 +8,7 @@
 
 syntax: regexp
 
+^contrib
 ^heaps/
 ^browser_info/
 ^doc-src/.*\.aux

--- a/Admin/isatest/isatest-makedist	Wed Jun 17 10:07:25 2009 +0200
+++ b/Admin/isatest/isatest-makedist	Wed Jun 17 10:08:06 2009 +0200
@@ -102,7 +102,7 @@
 #sleep 15
 $SSH macbroy22 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
 sleep 15
-$SSH macbroy23 "$MAKEALL $HOME/settings/at-sml-dev-e"
+$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
 sleep 15
 $SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15

--- a/Admin/isatest/isatest-statistics	Wed Jun 17 10:07:25 2009 +0200
+++ b/Admin/isatest/isatest-statistics	Wed Jun 17 10:08:06 2009 +0200
@@ -51,7 +51,7 @@
 SESSIONS="$@"
 
 case "$PLATFORM" in
-  *para*)
+  *para* | *-M*)
     PARALLEL=true
     ;;
   *)

--- a/Admin/isatest/settings/mac-poly-M8	Wed Jun 17 10:07:25 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M8	Wed Jun 17 10:08:06 2009 +0200
@@ -4,7 +4,7 @@
   ML_SYSTEM="polyml-experimental"
   ML_PLATFORM="x86-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="--mutable 800 --immutable 2000"
+  ML_OPTIONS="--mutable 600 --immutable 1800"
 
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly-M8

--- a/NEWS	Wed Jun 17 10:07:25 2009 +0200
+++ b/NEWS	Wed Jun 17 10:08:06 2009 +0200
@@ -40,6 +40,9 @@
 * Implementation of quickcheck using generic code generator; default generators
 are provided for all suitable HOL types, records and datatypes.
 
+* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
+Set.Pow_def and Set.image_def.  INCOMPATIBILITY.
+
 
 *** ML ***
 

--- a/etc/settings	Wed Jun 17 10:07:25 2009 +0200
+++ b/etc/settings	Wed Jun 17 10:08:06 2009 +0200
@@ -91,8 +91,7 @@
 ### Batch sessions (cf. isabelle usedir)
 ###
 
-ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -v true -V outline=/proof,/ML"
-#ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
+ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
 
 # Specifically for the HOL image
 HOL_USEDIR_OPTIONS=""

--- a/src/HOL/Divides.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Divides.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -331,17 +331,22 @@
   "(a * c) mod (b * c) = (a mod b) * c"
   using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
 
-end
+lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
+  unfolding dvd_def by (auto simp add: mod_mult_mult1)
+
+lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
+by (blast intro: dvd_mod_imp_dvd dvd_mod)
 
 lemma div_power:
-  "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \<Longrightarrow>
-    (x div y) ^ n = x ^ n div y ^ n"
+  "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
 apply (induct n)
  apply simp
 apply(simp add: div_mult_div_if_dvd dvd_power_same)
 done
 
-class ring_div = semiring_div + comm_ring_1
+end
+
+class ring_div = semiring_div + idom
 begin
 
 text {* Negation respects modular equivalence. *}
@@ -905,15 +910,6 @@
   apply (rule dvd_refl)
   done
 
-lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
-  unfolding dvd_def
-  apply (case_tac "n = 0", auto)
-  apply (blast intro: mod_mult_distrib2 [symmetric])
-  done
-
-lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
-by (blast intro: dvd_mod_imp_dvd dvd_mod)
-
 lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
   unfolding dvd_def
   apply (erule exE)

--- a/src/HOL/IntDiv.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/IntDiv.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -1059,13 +1059,10 @@
 done
 
 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
-  by (auto elim!: dvdE simp add: mod_mult_mult1)
+  by (rule dvd_mod) (* TODO: remove *)
 
 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
-  apply (subgoal_tac "k dvd n * (m div n) + m mod n")
-   apply (simp add: zmod_zdiv_equality [symmetric])
-  apply (simp only: dvd_add dvd_mult2)
-  done
+  by (rule dvd_mod_imp_dvd) (* TODO: remove *)
 
 lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   apply (auto elim!: dvdE)

--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -46,7 +46,8 @@
         "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
   apply(rule_tac [!] setsum_cong2) using assms by auto
 
-lemma setsum_delta'': fixes s::"(real^'n) set" assumes "finite s"
+lemma setsum_delta'':
+  fixes s::"'a::real_vector set" assumes "finite s"
   shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *\<^sub>R x) = (if y\<in>s then (f y) *\<^sub>R y else 0)"
 proof-
   have *:"\<And>x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto
@@ -107,8 +108,8 @@
 subsection {* Affine set and affine hull.*}
 
 definition
-  affine :: "(real ^ 'n::finite) set \<Rightarrow> bool" where
-  "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v::real. u + v = 1 \<longrightarrow> (u *\<^sub>R x + v *\<^sub>R y) \<in> s)"
+  affine :: "'a::real_vector set \<Rightarrow> bool" where
+  "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
 
 lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
 proof- have *:"\<And>u v ::real. u + v = 1 \<longleftrightarrow> v = 1 - u" by auto
@@ -149,7 +150,7 @@
 
 subsection {* Some explicit formulations (from Lars Schewe). *}
 
-lemma affine: fixes V::"(real^'n::finite) set"
+lemma affine: fixes V::"'a::real_vector set"
   shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)"
 unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ 
 defer apply(rule, rule, rule, rule, rule) proof-
@@ -169,7 +170,7 @@
     thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5)
       by(auto simp add: setsum_clauses(2))
   next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s)
-      case (Suc n) fix s::"(real^'n) set" and u::"real^'n\<Rightarrow> real"
+      case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real"
       assume IA:"\<And>u s.  \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s;
                s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n \<equiv> card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and
 	as:"Suc n \<equiv> card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
@@ -251,7 +252,8 @@
   apply(rule hull_unique) unfolding mem_def by auto
 
 lemma affine_hull_finite_step:
-  shows "(\<exists>u::real^'n=>real. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
+  fixes y :: "'a::real_vector"
+  shows "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
   "finite s \<Longrightarrow> (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow>
                 (\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)")
 proof-
@@ -288,10 +290,12 @@
   ultimately show "?lhs = ?rhs" by blast
 qed
 
-lemma affine_hull_2:"affine hull {a,b::real^'n::finite} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs")
+lemma affine_hull_2:
+  fixes a b :: "'a::real_vector"
+  shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs")
 proof-
   have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
-         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real^'n)" by auto
+         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
   have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
     using affine_hull_finite[of "{a,b}"] by auto
   also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"
@@ -300,10 +304,12 @@
   finally show ?thesis by auto
 qed
 
-lemma affine_hull_3: "affine hull {a,b,c::real^'n::finite} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")
+lemma affine_hull_3:
+  fixes a b c :: "'a::real_vector"
+  shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")
 proof-
   have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)" 
-         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real^'n)" by auto
+         "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
   show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)
     unfolding * apply auto
     apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
@@ -313,7 +319,8 @@
 subsection {* Some relations between affine hull and subspaces. *}
 
 lemma affine_hull_insert_subset_span:
-  "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
+  fixes a :: "real ^ _"
+  shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
   unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq smult_conv_scaleR
   apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof-
   fix x t u assume as:"finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
@@ -330,6 +337,7 @@
     unfolding as by simp qed
 
 lemma affine_hull_insert_span:
+  fixes a :: "real ^ _"
   assumes "a \<notin> s"
   shows "affine hull (insert a s) =
             {a + v | v . v \<in> span {x - a | x.  x \<in> s}}"
@@ -349,14 +357,16 @@
     by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps) qed
 
 lemma affine_hull_span:
+  fixes a :: "real ^ _"
   assumes "a \<in> s"
   shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
   using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
 
 subsection {* Convexity. *}
 
-definition "convex (s::(real^'n::finite) set) \<longleftrightarrow>
-        (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. (u + v = 1) \<longrightarrow> (u *\<^sub>R x + v *\<^sub>R y) \<in> s)"
+definition
+  convex :: "'a::real_vector set \<Rightarrow> bool" where
+  "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
 
 lemma convex_alt: "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> ((1 - u) *\<^sub>R x + u *\<^sub>R y) \<in> s)"
 proof- have *:"\<And>u v::real. u + v = 1 \<longleftrightarrow> u = 1 - v" by auto
@@ -445,7 +455,9 @@
     thus ?thesis unfolding setsum_cl_ivl_Suc and *** and scaleR_right.setsum [symmetric] using nn by auto qed qed auto qed
 
 
-lemma convex_explicit: "convex (s::(real^'n::finite) set) \<longleftrightarrow>
+lemma convex_explicit:
+  fixes s :: "'a::real_vector set"
+  shows "convex s \<longleftrightarrow>
   (\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) t \<in> s)"
   unfolding convex_def apply(rule,rule,rule) apply(subst imp_conjL,rule) defer apply(rule,rule,rule,rule,rule,rule,rule) proof-
   fix x y u v assume as:"\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
@@ -453,7 +465,7 @@
     case True show ?thesis unfolding True and scaleR_left_distrib[THEN sym] using as(3,6) by auto next
     case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>z. if z=x then u else v"]] and as(2-) by auto qed
 next 
-  fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::(real^'n) set)"
+  fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::'a set)"
   (*"finite t" "t \<subseteq> s" "\<forall>x\<in>t. (0::real) \<le> u x" "setsum u t = 1"*)
   from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" apply(induct_tac t rule:finite_induct)
     prefer 3 apply (rule,rule) apply(erule conjE)+ proof-
@@ -493,7 +505,9 @@
 
 subsection {* Cones. *}
 
-definition "cone (s::(real^'n) set) \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)"
+definition
+  cone :: "'a::real_vector set \<Rightarrow> bool" where
+  "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)"
 
 lemma cone_empty[intro, simp]: "cone {}"
   unfolding cone_def by auto
@@ -517,7 +531,7 @@
 subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}
 
 definition
-  affine_dependent :: "(real ^ 'n::finite) set \<Rightarrow> bool" where
+  affine_dependent :: "'a::real_vector set \<Rightarrow> bool" where
   "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))"
 
 lemma affine_dependent_explicit:
@@ -537,21 +551,21 @@
   have "s \<noteq> {v}" using as(3,6) by auto
   thus "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x" 
     apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI)
-    unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1_ring[OF as(1,5)] using as by auto
+    unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as by auto
 qed
 
 lemma affine_dependent_explicit_finite:
-  assumes "finite (s::(real^'n::finite) set)"
+  fixes s :: "'a::real_vector set" assumes "finite s"
   shows "affine_dependent s \<longleftrightarrow> (\<exists>u. setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)"
   (is "?lhs = ?rhs")
 proof
-  have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::real^'n))" by auto
+  have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto
   assume ?lhs
   then obtain t u v where "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0"  "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
     unfolding affine_dependent_explicit by auto
   thus ?rhs apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
     apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym]
-    unfolding Int_absorb2[OF `t\<subseteq>s`, unfolded Int_commute] by auto
+    unfolding Int_absorb1[OF `t\<subseteq>s`] by auto
 next
   assume ?rhs
   then obtain u v where "setsum u s = 0"  "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" by auto
@@ -561,6 +575,7 @@
 subsection {* A general lemma. *}
 
 lemma convex_connected:
+  fixes s :: "'a::real_normed_vector set"
   assumes "convex s" shows "connected s"
 proof-
   { fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2" 
@@ -595,12 +610,14 @@
 
 subsection {* One rather trivial consequence. *}
 
-lemma connected_UNIV: "connected (UNIV :: (real ^ _) set)"
+lemma connected_UNIV: "connected (UNIV :: 'a::real_normed_vector set)"
   by(simp add: convex_connected convex_UNIV)
 
 subsection {* Convex functions into the reals. *}
 
-definition "convex_on s (f::real^'n \<Rightarrow> real) = 
+definition
+  convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" where
+  "convex_on s f \<longleftrightarrow>
   (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
 
 lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
@@ -641,6 +658,7 @@
 qed
 
 lemma convex_local_global_minimum:
+  fixes s :: "'a::real_normed_vector set"
   assumes "0<e" "convex_on s f" "ball x e \<subseteq> s" "\<forall>y\<in>ball x e. f x \<le> f y"
   shows "\<forall>y\<in>s. f x \<le> f y"
 proof(rule ccontr)
@@ -661,7 +679,9 @@
   ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
 qed
 
-lemma convex_distance: "convex_on s (\<lambda>x. dist a x)"
+lemma convex_distance:
+  fixes s :: "'a::real_normed_vector set"
+  shows "convex_on s (\<lambda>x. dist a x)"
 proof(auto simp add: convex_on_def dist_norm)
   fix x y assume "x\<in>s" "y\<in>s"
   fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
@@ -710,23 +730,28 @@
 proof- have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto
   thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed
 
-lemma convex_affinity: assumes "convex (s::(real^'n::finite) set)" shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
+lemma convex_affinity: assumes "convex s" shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof- have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto
   thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed
 
-lemma convex_linear_image: assumes c:"convex s" and l:"linear f" shows "convex(f ` s)"
+lemma convex_linear_image:
+  assumes c:"convex s" and l:"bounded_linear f"
+  shows "convex(f ` s)"
 proof(auto simp add: convex_def)
+  interpret f: bounded_linear f by fact
   fix x y assume xy:"x \<in> s" "y \<in> s"
   fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
   show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff
     apply(rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in bexI)
-    unfolding linear_add[OF l] linear_cmul[OF l, unfolded smult_conv_scaleR] 
+    unfolding f.add f.scaleR
     using c[unfolded convex_def] xy uv by auto
 qed
 
 subsection {* Balls, being convex, are connected. *}
 
-lemma convex_ball: "convex (ball x e)" 
+lemma convex_ball:
+  fixes x :: "'a::real_normed_vector"
+  shows "convex (ball x e)" 
 proof(auto simp add: convex_def)
   fix y z assume yz:"dist x y < e" "dist x z < e"
   fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
@@ -735,7 +760,9 @@
   thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using real_convex_bound_lt[OF yz uv] by auto 
 qed
 
-lemma convex_cball: "convex(cball x e)"
+lemma convex_cball:
+  fixes x :: "'a::real_normed_vector"
+  shows "convex(cball x e)"
 proof(auto simp add: convex_def Ball_def mem_cball)
   fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e"
   fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
@@ -744,10 +771,14 @@
   thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using real_convex_bound_le[OF yz uv] by auto 
 qed
 
-lemma connected_ball: "connected(ball (x::real^_) e)" (* FIXME: generalize *)
+lemma connected_ball:
+  fixes x :: "'a::real_normed_vector"
+  shows "connected (ball x e)"
   using convex_connected convex_ball by auto
 
-lemma connected_cball: "connected(cball (x::real^_) e)" (* FIXME: generalize *)
+lemma connected_cball:
+  fixes x :: "'a::real_normed_vector"
+  shows "connected(cball x e)"
   using convex_connected convex_cball by auto
 
 subsection {* Convex hull. *}
@@ -759,14 +790,17 @@
 lemma convex_hull_eq: "(convex hull s = s) \<longleftrightarrow> convex s" apply(rule hull_eq[unfolded mem_def])
   using convex_Inter[unfolded Ball_def mem_def] by auto
 
-lemma bounded_convex_hull: assumes "bounded s" shows "bounded(convex hull s)"
+lemma bounded_convex_hull:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "bounded s" shows "bounded(convex hull s)"
 proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
   show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
     unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
     unfolding subset_eq mem_cball dist_norm using B by auto qed
 
 lemma finite_imp_bounded_convex_hull:
-  "finite s \<Longrightarrow> bounded(convex hull s)"
+  fixes s :: "'a::real_normed_vector set"
+  shows "finite s \<Longrightarrow> bounded(convex hull s)"
   using bounded_convex_hull finite_imp_bounded by auto
 
 subsection {* Stepping theorems for convex hulls of finite sets. *}
@@ -778,6 +812,7 @@
   apply(rule hull_unique) unfolding mem_def by auto
 
 lemma convex_hull_insert:
+  fixes s :: "'a::real_vector set"
   assumes "s \<noteq> {}"
   shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
                                     b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
@@ -797,10 +832,10 @@
     fix x y u v assume as:"(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
     from as(4) obtain u1 v1 b1 where obt1:"u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
     from as(5) obtain u2 v2 b2 where obt2:"u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
-    have *:"\<And>(x::real^_) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
+    have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
     have "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
     proof(cases "u * v1 + v * v2 = 0")
-      have *:"\<And>(x::real^_) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
+      have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
       case True hence **:"u * v1 = 0" "v * v2 = 0" apply- apply(rule_tac [!] ccontr)
 	using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by auto
       hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto
@@ -834,7 +869,8 @@
 subsection {* Explicit expression for convex hull. *}
 
 lemma convex_hull_indexed:
-  "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
+  fixes s :: "'a::real_vector set"
+  shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
                             (setsum u {1..k} = 1) \<and>
                             (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
   apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer
@@ -852,7 +888,7 @@
   fix x y u v assume uv:"0\<le>u" "0\<le>v" "u+v=(1::real)" and xy:"x\<in>?hull" "y\<in>?hull"
   from xy obtain k1 u1 x1 where x:"\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto
   from xy obtain k2 u2 x2 where y:"\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto
-  have *:"\<And>P x1 x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
+  have *:"\<And>P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
     "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
     prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le)
   have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto  
@@ -873,7 +909,8 @@
 qed
 
 lemma convex_hull_finite:
-  assumes "finite (s::(real^'n::finite)set)"
+  fixes s :: "'a::real_vector set"
+  assumes "finite s"
   shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
          setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
 proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])
@@ -902,8 +939,17 @@
 
 subsection {* Another formulation from Lars Schewe. *}
 
+lemma setsum_constant_scaleR:
+  fixes y :: "'a::real_vector"
+  shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
+apply (cases "finite A")
+apply (induct set: finite)
+apply (simp_all add: algebra_simps)
+done
+
 lemma convex_hull_explicit:
-  "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
+  fixes p :: "'a::real_vector set"
+  shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
              (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
 proof-
   { fix x assume "x\<in>?lhs"
@@ -940,7 +986,9 @@
       then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto
       hence "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto
       hence "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
-      hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y" "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" by auto   }
+      hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
+            "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
+        by (auto simp add: setsum_constant_scaleR)   }
 
     hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
       unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f] 
@@ -956,7 +1004,7 @@
 subsection {* A stepping theorem for that expansion. *}
 
 lemma convex_hull_finite_step:
-  assumes "finite (s::(real^'n) set)"
+  fixes s :: "'a::real_vector set" assumes "finite s"
   shows "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y)
      \<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs")
 proof(rule, case_tac[!] "a\<in>s")
@@ -995,7 +1043,7 @@
     unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed
 
 lemma convex_hull_3:
-  "convex hull {a::real^'n::finite,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}"
+  "convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}"
 proof-
   have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
   have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
@@ -1013,20 +1061,27 @@
 
 subsection {* Relations among closure notions and corresponding hulls. *}
 
-lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
+text {* TODO: Generalize linear algebra concepts defined in @{text
+Euclidean_Space.thy} so that we can generalize these lemmas. *}
+
+lemma subspace_imp_affine:
+  fixes s :: "(real ^ _) set" shows "subspace s \<Longrightarrow> affine s"
   unfolding subspace_def affine_def smult_conv_scaleR by auto
 
 lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
   unfolding affine_def convex_def by auto
 
-lemma subspace_imp_convex: "subspace s \<Longrightarrow> convex s"
+lemma subspace_imp_convex:
+  fixes s :: "(real ^ _) set" shows "subspace s \<Longrightarrow> convex s"
   using subspace_imp_affine affine_imp_convex by auto
 
-lemma affine_hull_subset_span: "(affine hull s) \<subseteq> (span s)"
+lemma affine_hull_subset_span:
+  fixes s :: "(real ^ _) set" shows "(affine hull s) \<subseteq> (span s)"
   unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
   using subspace_imp_affine  by auto
 
-lemma convex_hull_subset_span: "(convex hull s) \<subseteq> (span s)"
+lemma convex_hull_subset_span:
+  fixes s :: "(real ^ _) set" shows "(convex hull s) \<subseteq> (span s)"
   unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
   using subspace_imp_convex by auto
 
@@ -1034,11 +1089,13 @@
   unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
   using affine_imp_convex by auto
 
-lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
+lemma affine_dependent_imp_dependent:
+  fixes s :: "(real ^ _) set" shows "affine_dependent s \<Longrightarrow> dependent s"
   unfolding affine_dependent_def dependent_def 
   using affine_hull_subset_span by auto
 
 lemma dependent_imp_affine_dependent:
+  fixes s :: "(real ^ _) set"
   assumes "dependent {x - a| x . x \<in> s}" "a \<notin> s"
   shows "affine_dependent (insert a s)"
 proof-
@@ -1188,6 +1245,7 @@
 subsection {* Openness and compactness are preserved by convex hull operation. *}
 
 lemma open_convex_hull:
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s"
   shows "open(convex hull s)"
   unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10) 
@@ -1255,7 +1313,7 @@
 qed
 
 lemma compact_convex_combinations:
-  fixes s t :: "(real ^ 'n::finite) set"
+  fixes s t :: "'a::real_normed_vector set"
   assumes "compact s" "compact t"
   shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
 proof-
@@ -1351,13 +1409,14 @@
 qed
 
 lemma finite_imp_compact_convex_hull:
- "finite s \<Longrightarrow> compact(convex hull s)"
+  fixes s :: "(real ^ _) set"
+  shows "finite s \<Longrightarrow> compact(convex hull s)"
   apply(drule finite_imp_compact, drule compact_convex_hull) by assumption
 
 subsection {* Extremal points of a simplex are some vertices. *}
 
 lemma dist_increases_online:
-  fixes a b d :: "real ^ 'n::finite"
+  fixes a b d :: "'a::real_inner"
   assumes "d \<noteq> 0"
   shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
 proof(cases "inner a d - inner b d > 0")
@@ -1373,11 +1432,12 @@
 qed
 
 lemma norm_increases_online:
- "(d::real^'n::finite) \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
+  fixes d :: "'a::real_inner"
+  shows "d \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
   using dist_increases_online[of d a 0] unfolding dist_norm by auto
 
 lemma simplex_furthest_lt:
-  fixes s::"(real^'n::finite) set" assumes "finite s"
+  fixes s::"'a::real_inner set" assumes "finite s"
   shows "\<forall>x \<in> (convex hull s).  x \<notin> s \<longrightarrow> (\<exists>y\<in>(convex hull s). norm(x - a) < norm(y - a))"
 proof(induct_tac rule: finite_induct[of s])
   fix x s assume as:"finite s" "x\<notin>s" "\<forall>x\<in>convex hull s. x \<notin> s \<longrightarrow> (\<exists>y\<in>convex hull s. norm (x - a) < norm (y - a))"
@@ -1432,6 +1492,7 @@
 qed (auto simp add: assms)
 
 lemma simplex_furthest_le:
+  fixes s :: "(real ^ _) set"
   assumes "finite s" "s \<noteq> {}"
   shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x - a) \<le> norm(y - a)"
 proof-
@@ -1447,10 +1508,12 @@
 qed
 
 lemma simplex_furthest_le_exists:
-  "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
+  fixes s :: "(real ^ _) set"
+  shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
   using simplex_furthest_le[of s] by (cases "s={}")auto
 
 lemma simplex_extremal_le:
+  fixes s :: "(real ^ _) set"
   assumes "finite s" "s \<noteq> {}"
   shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x - y) \<le> norm(u - v)"
 proof-
@@ -1471,7 +1534,8 @@
 qed 
 
 lemma simplex_extremal_le_exists:
-  "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
+  fixes s :: "(real ^ _) set"
+  shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
   \<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x - y) \<le> norm(u - v))"
   using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto
 
@@ -1532,6 +1596,7 @@
     unfolding dist_norm by(auto simp add: norm_minus_commute field_simps) qed
 
 lemma any_closest_point_dot:
+  fixes s :: "(real ^ _) set"
   assumes "convex s" "closed s" "x \<in> s" "y \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
   shows "inner (a - x) (y - x) \<le> 0"
 proof(rule ccontr) assume "\<not> inner (a - x) (y - x) \<le> 0"
@@ -1552,6 +1617,7 @@
 qed
 
 lemma any_closest_point_unique:
+  fixes s :: "(real ^ _) set"
   assumes "convex s" "closed s" "x \<in> s" "y \<in> s"
   "\<forall>z\<in>s. dist a x \<le> dist a z" "\<forall>z\<in>s. dist a y \<le> dist a z"
   shows "x = y" using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)]
@@ -1603,6 +1669,7 @@
 subsection {* Various point-to-set separating/supporting hyperplane theorems. *}
 
 lemma supporting_hyperplane_closed_point:
+  fixes s :: "(real ^ _) set"
   assumes "convex s" "closed s" "s \<noteq> {}" "z \<notin> s"
   shows "\<exists>a b. \<exists>y\<in>s. inner a z < b \<and> (inner a y = b) \<and> (\<forall>x\<in>s. inner a x \<ge> b)"
 proof-
@@ -1621,6 +1688,7 @@
 qed
 
 lemma separating_hyperplane_closed_point:
+  fixes s :: "(real ^ _) set"
   assumes "convex s" "closed s" "z \<notin> s"
   shows "\<exists>a b. inner a z < b \<and> (\<forall>x\<in>s. inner a x > b)"
 proof(cases "s={}")
@@ -1691,6 +1759,7 @@
 qed
 
 lemma separating_hyperplane_compact_closed:
+  fixes s :: "(real ^ _) set"
   assumes "convex s" "compact s" "s \<noteq> {}" "convex t" "closed t" "s \<inter> t = {}"
   shows "\<exists>a b. (\<forall>x\<in>s. inner a x < b) \<and> (\<forall>x\<in>t. inner a x > b)"
 proof- obtain a b where "(\<forall>x\<in>t. inner a x < b) \<and> (\<forall>x\<in>s. b < inner a x)"
@@ -1733,14 +1802,18 @@
 
 subsection {* More convexity generalities. *}
 
-lemma convex_closure: assumes "convex s" shows "convex(closure s)"
+lemma convex_closure:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "convex s" shows "convex(closure s)"
   unfolding convex_def Ball_def closure_sequential
   apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
   apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
   apply(rule assms[unfolded convex_def, rule_format]) prefer 6
   apply(rule Lim_add) apply(rule_tac [1-2] Lim_cmul) by auto
 
-lemma convex_interior: assumes "convex s" shows "convex(interior s)"
+lemma convex_interior:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "convex s" shows "convex(interior s)"
   unfolding convex_alt Ball_def mem_interior apply(rule,rule,rule,rule,rule,rule) apply(erule exE | erule conjE)+ proof-
   fix x y u assume u:"0 \<le> u" "u \<le> (1::real)"
   fix e d assume ed:"ball x e \<subseteq> s" "ball y d \<subseteq> s" "0<d" "0<e" 
@@ -1789,6 +1862,7 @@
 subsection {* Convex set as intersection of halfspaces. *}
 
 lemma convex_halfspace_intersection:
+  fixes s :: "(real ^ _) set"
   assumes "closed s" "convex s"
   shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
   apply(rule set_ext, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof- 
@@ -1915,20 +1989,23 @@
 subsection {* Convex hull is "preserved" by a linear function. *}
 
 lemma convex_hull_linear_image:
-  assumes "linear f"
+  assumes "bounded_linear f"
   shows "f ` (convex hull s) = convex hull (f ` s)"
   apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3  
   apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
   apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
-proof- show "convex {x. f x \<in> convex hull f ` s}" 
-  unfolding convex_def by(auto simp add: linear_cmul[OF assms, unfolded smult_conv_scaleR]  linear_add[OF assms]
-    convex_convex_hull[unfolded convex_def, rule_format]) next
+proof-
+  interpret f: bounded_linear f by fact
+  show "convex {x. f x \<in> convex hull f ` s}" 
+  unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
+  interpret f: bounded_linear f by fact
   show "convex {x. x \<in> f ` (convex hull s)}" using  convex_convex_hull[unfolded convex_def, of s] 
-    unfolding convex_def by (auto simp add: linear_cmul[OF assms, THEN sym, unfolded smult_conv_scaleR]  linear_add[OF assms, THEN sym])
+    unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
 qed auto
 
 lemma in_convex_hull_linear_image:
-  assumes "linear f" "x \<in> convex hull s" shows "(f x) \<in> convex hull (f ` s)"
+  assumes "bounded_linear f" "x \<in> convex hull s"
+  shows "(f x) \<in> convex hull (f ` s)"
 using convex_hull_linear_image[OF assms(1)] assms(2) by auto
 
 subsection {* Homeomorphism of all convex compact sets with nonempty interior. *}
@@ -2188,6 +2265,7 @@
   apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
 
 lemma convex_on:
+  fixes s :: "(real ^ _) set"
   assumes "convex s"
   shows "convex_on s f \<longleftrightarrow> (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow>
    f (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} ) \<le> setsum (\<lambda>i. u i * f(x i)) {1..k} ) "
@@ -2203,7 +2281,9 @@
 
 subsection {* Convexity of general and special intervals. *}
 
-lemma is_interval_convex: assumes "is_interval s" shows "convex s"
+lemma is_interval_convex:
+  fixes s :: "(real ^ _) set"
+  assumes "is_interval s" shows "convex s"
   unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-
   fix x y u v assume as:"x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
   hence *:"u = 1 - v" "1 - v \<ge> 0" and **:"v = 1 - u" "1 - u \<ge> 0" by auto
@@ -2288,6 +2368,7 @@
 subsection {* A bound within a convex hull, and so an interval. *}
 
 lemma convex_on_convex_hull_bound:
+  fixes s :: "(real ^ _) set"
   assumes "convex_on (convex hull s) f" "\<forall>x\<in>s. f x \<le> b"
   shows "\<forall>x\<in> convex hull s. f x \<le> b" proof
   fix x assume "x\<in>convex hull s"
@@ -2390,6 +2471,7 @@
 subsection {* Bounded convex function on open set is continuous. *}
 
 lemma convex_on_bounded_continuous:
+  fixes s :: "(real ^ _) set"
   assumes "open s" "convex_on s f" "\<forall>x\<in>s. abs(f x) \<le> b"
   shows "continuous_on s f"
   apply(rule continuous_at_imp_continuous_on) unfolding continuous_at_real_range proof(rule,rule,rule)
@@ -2440,6 +2522,7 @@
 subsection {* Upper bound on a ball implies upper and lower bounds. *}
 
 lemma convex_bounds_lemma:
+  fixes x :: "real ^ _"
   assumes "convex_on (cball x e) f"  "\<forall>y \<in> cball x e. f y \<le> b"
   shows "\<forall>y \<in> cball x e. abs(f y) \<le> b + 2 * abs(f x)"
   apply(rule) proof(cases "0 \<le> e") case True
@@ -2619,6 +2702,7 @@
 subsection {* Shrinking towards the interior of a convex set. *}
 
 lemma mem_interior_convex_shrink:
+  fixes s :: "(real ^ _) set"
   assumes "convex s" "c \<in> interior s" "x \<in> s" "0 < e" "e \<le> 1"
   shows "x - e *\<^sub>R (x - c) \<in> interior s"
 proof- obtain d where "d>0" and d:"ball c d \<subseteq> s" using assms(2) unfolding mem_interior by auto
@@ -2637,6 +2721,7 @@
   qed(rule mult_pos_pos, insert `e>0` `d>0`, auto) qed
 
 lemma mem_interior_closure_convex_shrink:
+  fixes s :: "(real ^ _) set"
   assumes "convex s" "c \<in> interior s" "x \<in> closure s" "0 < e" "e \<le> 1"
   shows "x - e *\<^sub>R (x - c) \<in> interior s"
 proof- obtain d where "d>0" and d:"ball c d \<subseteq> s" using assms(2) unfolding mem_interior by auto

--- a/src/HOL/Library/Euclidean_Space.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -889,7 +889,7 @@
 subsection {* A connectedness or intermediate value lemma with several applications. *}
 
 lemma connected_real_lemma:
-  fixes f :: "real \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "real \<Rightarrow> 'a::metric_space"
   assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
   and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
   and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"

--- a/src/HOL/Library/Fin_Fun.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -323,13 +323,13 @@
 
 primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
     "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
-       [(1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+       [(1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
   | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight
-       [(Suc_code_numeral i, random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun_aux i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
-         (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+       [(Suc_code_numeral i, Quickcheck.random j o\<rightarrow> (\<lambda>x. Quickcheck.random j o\<rightarrow> (\<lambda>y. random_finfun_aux i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
+         (1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
 
 definition 
-  "random i = random_finfun_aux i i"
+  "Quickcheck.random i = random_finfun_aux i i"
 
 instance ..
 
@@ -337,8 +337,8 @@
 
 lemma random_finfun_aux_code [code]:
   "random_finfun_aux i j = Quickcheck.collapse (Random.select_weight
-     [(i, random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun_aux (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
-       (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+     [(i, Quickcheck.random j o\<rightarrow> (\<lambda>x. Quickcheck.random j o\<rightarrow> (\<lambda>y. random_finfun_aux (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
+       (1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
   apply (cases i rule: code_numeral.exhaust)
   apply (simp_all only: random_finfun_aux.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
   apply (subst select_weight_cons_zero) apply (simp only:)

--- a/src/HOL/Library/Polynomial.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -632,6 +632,25 @@
   shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
   by (safe elim!: dvd_smult dvd_smult_cancel)
 
+lemma smult_dvd_cancel:
+  "smult a p dvd q \<Longrightarrow> p dvd q"
+proof -
+  assume "smult a p dvd q"
+  then obtain k where "q = smult a p * k" ..
+  then have "q = p * smult a k" by simp
+  then show "p dvd q" ..
+qed
+
+lemma smult_dvd:
+  fixes a :: "'a::field"
+  shows "p dvd q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> smult a p dvd q"
+  by (rule smult_dvd_cancel [where a="inverse a"]) simp
+
+lemma smult_dvd_iff:
+  fixes a :: "'a::field"
+  shows "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
+  by (auto elim: smult_dvd smult_dvd_cancel)
+
 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
 by (induct n, simp, auto intro: order_trans degree_mult_le)
 
@@ -1102,6 +1121,109 @@
 done
 
 
+subsection {* GCD of polynomials *}
+
+function
+  poly_gcd :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
+  "poly_gcd x 0 = smult (inverse (coeff x (degree x))) x"
+| "y \<noteq> 0 \<Longrightarrow> poly_gcd x y = poly_gcd y (x mod y)"
+by auto
+
+termination poly_gcd
+by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
+   (auto dest: degree_mod_less)
+
+declare poly_gcd.simps [simp del, code del]
+
+lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x"
+  and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
+  apply (induct x y rule: poly_gcd.induct)
+  apply (simp_all add: poly_gcd.simps)
+  apply (fastsimp simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
+  apply (blast dest: dvd_mod_imp_dvd)
+  done
+
+lemma poly_gcd_greatest: "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd poly_gcd x y"
+  by (induct x y rule: poly_gcd.induct)
+     (simp_all add: poly_gcd.simps dvd_mod dvd_smult)
+
+lemma dvd_poly_gcd_iff [iff]:
+  "k dvd poly_gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
+  by (blast intro!: poly_gcd_greatest intro: dvd_trans)
+
+lemma poly_gcd_monic:
+  "coeff (poly_gcd x y) (degree (poly_gcd x y)) =
+    (if x = 0 \<and> y = 0 then 0 else 1)"
+  by (induct x y rule: poly_gcd.induct)
+     (simp_all add: poly_gcd.simps nonzero_imp_inverse_nonzero)
+
+lemma poly_gcd_zero_iff [simp]:
+  "poly_gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+  by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
+
+lemma poly_gcd_0_0 [simp]: "poly_gcd 0 0 = 0"
+  by simp
+
+lemma poly_dvd_antisym:
+  fixes p q :: "'a::idom poly"
+  assumes coeff: "coeff p (degree p) = coeff q (degree q)"
+  assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
+proof (cases "p = 0")
+  case True with coeff show "p = q" by simp
+next
+  case False with coeff have "q \<noteq> 0" by auto
+  have degree: "degree p = degree q"
+    using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0`
+    by (intro order_antisym dvd_imp_degree_le)
+
+  from `p dvd q` obtain a where a: "q = p * a" ..
+  with `q \<noteq> 0` have "a \<noteq> 0" by auto
+  with degree a `p \<noteq> 0` have "degree a = 0"
+    by (simp add: degree_mult_eq)
+  with coeff a show "p = q"
+    by (cases a, auto split: if_splits)
+qed
+
+lemma poly_gcd_unique:
+  assumes dvd1: "d dvd x" and dvd2: "d dvd y"
+    and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
+    and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
+  shows "poly_gcd x y = d"
+proof -
+  have "coeff (poly_gcd x y) (degree (poly_gcd x y)) = coeff d (degree d)"
+    by (simp_all add: poly_gcd_monic monic)
+  moreover have "poly_gcd x y dvd d"
+    using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
+  moreover have "d dvd poly_gcd x y"
+    using dvd1 dvd2 by (rule poly_gcd_greatest)
+  ultimately show ?thesis
+    by (rule poly_dvd_antisym)
+qed
+
+lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x"
+by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+
+lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
+by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
+
+lemmas poly_gcd_left_commute =
+  mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
+
+lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
+
+lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1"
+by (rule poly_gcd_unique) simp_all
+
+lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1"
+by (rule poly_gcd_unique) simp_all
+
+lemma poly_gcd_minus_left [simp]: "poly_gcd (- x) y = poly_gcd x y"
+by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+
+lemma poly_gcd_minus_right [simp]: "poly_gcd x (- y) = poly_gcd x y"
+by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+
+
 subsection {* Evaluation of polynomials *}
 
 definition
@@ -1472,4 +1594,10 @@
 apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
 done
 
+lemma poly_gcd_code [code]:
+  "poly_gcd x y =
+    (if y = 0 then smult (inverse (coeff x (degree x))) x
+              else poly_gcd y (x mod y))"
+  by (simp add: poly_gcd.simps)
+
 end

--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -1102,7 +1102,7 @@
 
   text{* Notation Lim to avoid collition with lim defined in analysis *}
 definition
-  Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b" where
+  Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b" where
   "Lim net f = (THE l. (f ---> l) net)"
 
 lemma Lim:
@@ -1238,11 +1238,10 @@
 
 text{* Basic arithmetical combining theorems for limits. *}
 
-lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
-  assumes "(f ---> l) net" "linear h"
+lemma Lim_linear:
+  assumes "(f ---> l) net" "bounded_linear h"
   shows "((\<lambda>x. h (f x)) ---> h l) net"
-using `linear h` `(f ---> l) net`
-unfolding linear_conv_bounded_linear
+using `bounded_linear h` `(f ---> l) net`
 by (rule bounded_linear.tendsto)
 
 lemma Lim_ident_at: "((\<lambda>x. x) ---> a) (at a)"
@@ -1252,7 +1251,7 @@
   by (rule tendsto_const)
 
 lemma Lim_cmul:
-  fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   shows "(f ---> l) net ==> ((\<lambda>x. c *\<^sub>R f x) ---> c *\<^sub>R l) net"
   by (intro tendsto_intros)
 
@@ -1402,47 +1401,41 @@
 text{* Uniqueness of the limit, when nontrivial. *}
 
 lemma Lim_unique:
-  fixes f :: "'a \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a \<Rightarrow> 'b::t2_space"
   assumes "\<not> trivial_limit net"  "(f ---> l) net"  "(f ---> l') net"
   shows "l = l'"
 proof (rule ccontr)
-  let ?d = "dist l l' / 2"
   assume "l \<noteq> l'"
-  then have "0 < ?d" by (simp add: dist_nz)
-  have "eventually (\<lambda>x. dist (f x) l < ?d) net"
-    using `(f ---> l) net` `0 < ?d` by (rule tendstoD)
+  obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
+    using hausdorff [OF `l \<noteq> l'`] by fast
+  have "eventually (\<lambda>x. f x \<in> U) net"
+    using `(f ---> l) net` `open U` `l \<in> U` by (rule topological_tendstoD)
   moreover
-  have "eventually (\<lambda>x. dist (f x) l' < ?d) net"
-    using `(f ---> l') net` `0 < ?d` by (rule tendstoD)
+  have "eventually (\<lambda>x. f x \<in> V) net"
+    using `(f ---> l') net` `open V` `l' \<in> V` by (rule topological_tendstoD)
   ultimately
   have "eventually (\<lambda>x. False) net"
   proof (rule eventually_elim2)
     fix x
-    assume *: "dist (f x) l < ?d" "dist (f x) l' < ?d"
-    have "dist l l' \<le> dist (f x) l + dist (f x) l'"
-      by (rule dist_triangle_alt)
-    also from * have "\<dots> < ?d + ?d"
-      by (rule add_strict_mono)
-    also have "\<dots> = dist l l'" by simp
-    finally show "False" by simp
+    assume "f x \<in> U" "f x \<in> V"
+    hence "f x \<in> U \<inter> V" by simp
+    with `U \<inter> V = {}` show "False" by simp
   qed
   with `\<not> trivial_limit net` show "False"
     by (simp add: eventually_False)
 qed
 
 lemma tendsto_Lim:
-  fixes f :: "'a \<Rightarrow> 'b::metric_space"
+  fixes f :: "'a \<Rightarrow> 'b::t2_space"
   shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
   unfolding Lim_def using Lim_unique[of net f] by auto
 
 text{* Limit under bilinear function *}
 
 lemma Lim_bilinear:
-  fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
-  assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h"
+  assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
-using `bilinear h` `(f ---> l) net` `(g ---> m) net`
-unfolding bilinear_conv_bounded_bilinear
+using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net`
 by (rule bounded_bilinear.tendsto)
 
 text{* These are special for limits out of the same vector space. *}
@@ -1496,29 +1489,19 @@
 text{* It's also sometimes useful to extract the limit point from the net.  *}
 
 definition
-  netlimit :: "'a::metric_space net \<Rightarrow> 'a" where
-  "netlimit net = (SOME a. \<forall>r>0. eventually (\<lambda>x. dist x a < r) net)"
+  netlimit :: "'a::t2_space net \<Rightarrow> 'a" where
+  "netlimit net = (SOME a. ((\<lambda>x. x) ---> a) net)"
 
 lemma netlimit_within:
   assumes "\<not> trivial_limit (at a within S)"
   shows "netlimit (at a within S) = a"
-using assms
-apply (simp add: trivial_limit_within)
-apply (simp add: netlimit_def eventually_within zero_less_dist_iff)
-apply (rule some_equality, fast)
-apply (rename_tac b)
-apply (rule ccontr)
-apply (drule_tac x="dist b a / 2" in spec, drule mp, simp add: dist_nz)
-apply (clarify, rename_tac r)
-apply (simp only: islimpt_approachable)
-apply (drule_tac x="min r (dist b a / 2)" in spec, drule mp, simp add: dist_nz)
-apply (clarify)
-apply (drule_tac x=x' in bspec, simp)
-apply (drule mp, simp)
-apply (subgoal_tac "dist b a < dist b a / 2 + dist b a / 2", simp)
-apply (rule le_less_trans [OF dist_triangle3])
-apply (erule add_strict_mono)
-apply simp
+unfolding netlimit_def
+apply (rule some_equality)
+apply (rule Lim_at_within)
+apply (rule Lim_ident_at)
+apply (erule Lim_unique [OF assms])
+apply (rule Lim_at_within)
+apply (rule Lim_ident_at)
 done
 
 lemma netlimit_at:
@@ -2078,12 +2061,11 @@
 qed
 
 lemma bounded_linear_image:
-  fixes f :: "real^'m::finite \<Rightarrow> real^'n::finite"
-  assumes "bounded S" "linear f"
+  assumes "bounded S" "bounded_linear f"
   shows "bounded(f ` S)"
 proof-
   from assms(1) obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
-  from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x"  using linear_bounded_pos by auto
+  from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac)
   { fix x assume "x\<in>S"
     hence "norm x \<le> b" using b by auto
     hence "norm (f x) \<le> B * b" using B(2) apply(erule_tac x=x in allE)
@@ -2094,10 +2076,9 @@
 qed
 
 lemma bounded_scaling:
-  fixes S :: "(real ^ 'n::finite) set"
+  fixes S :: "'a::real_normed_vector set"
   shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
   apply (rule bounded_linear_image, assumption)
-  apply (simp only: linear_conv_bounded_linear)
   apply (rule scaleR.bounded_linear_right)
   done
 
@@ -3148,17 +3129,16 @@
 subsection{* Define continuity over a net to take in restrictions of the set. *}
 
 definition
-  continuous :: "'a::metric_space net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
+  continuous :: "'a::t2_space net \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
   "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
-  (* FIXME: generalize 'b to topological_space *)
 
 lemma continuous_trivial_limit:
  "trivial_limit net ==> continuous net f"
-  unfolding continuous_def tendsto_iff trivial_limit_eq by auto
+  unfolding continuous_def tendsto_def trivial_limit_eq by auto
 
 lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
   unfolding continuous_def
-  unfolding tendsto_iff
+  unfolding tendsto_def
   using netlimit_within[of x s]
   by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
 
@@ -3166,17 +3146,9 @@
   using continuous_within [of x UNIV f] by (simp add: within_UNIV)
 
 lemma continuous_at_within:
-  fixes x :: "'a::perfect_space"
   assumes "continuous (at x) f"  shows "continuous (at x within s) f"
-  (* FIXME: generalize *)
-proof(cases "x islimpt s")
-  case True show ?thesis using assms unfolding continuous_def and netlimit_at
-    using Lim_at_within[of f "f x" "at x" s]
-    unfolding netlimit_within[unfolded trivial_limit_within not_not, OF True] by blast
-next
-  case False thus ?thesis unfolding continuous_def and netlimit_at
-    unfolding Lim and trivial_limit_within by auto
-qed
+  using assms unfolding continuous_at continuous_within
+  by (rule Lim_at_within)
 
 text{* Derive the epsilon-delta forms, which we often use as "definitions" *}
 
@@ -3308,8 +3280,10 @@
 
 text{* Characterization of various kinds of continuity in terms of sequences.  *}
 
+(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
 lemma continuous_within_sequentially:
- "continuous (at a within s) f \<longleftrightarrow>
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows "continuous (at a within s) f \<longleftrightarrow>
                 (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
                      --> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
 proof
@@ -3349,7 +3323,8 @@
 qed
 
 lemma continuous_at_sequentially:
- "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
                   --> ((f o x) ---> f a) sequentially)"
   using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
 
@@ -3449,22 +3424,22 @@
   by (auto simp add: continuous_def Lim_const)
 
 lemma continuous_cmul:
-  fixes f :: "'a::metric_space \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
   by (auto simp add: continuous_def Lim_cmul)
 
 lemma continuous_neg:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
   by (auto simp add: continuous_def Lim_neg)
 
 lemma continuous_add:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
   by (auto simp add: continuous_def Lim_add)
 
 lemma continuous_sub:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
   by (auto simp add: continuous_def Lim_sub)
 
@@ -3475,7 +3450,7 @@
   unfolding continuous_on_eq_continuous_within using continuous_const by blast
 
 lemma continuous_on_cmul:
-  fixes f :: "'a::metric_space \<Rightarrow> real ^ _"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f ==>  continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
   unfolding continuous_on_eq_continuous_within using continuous_cmul by blast
 
@@ -3503,7 +3478,8 @@
   unfolding uniformly_continuous_on_def by simp
 
 lemma uniformly_continuous_on_cmul:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+    (* FIXME: generalize 'a to metric_space *)
   assumes "uniformly_continuous_on s f"
   shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
 proof-
@@ -3551,11 +3527,11 @@
 
 lemma continuous_within_id:
  "continuous (at a within s) (\<lambda>x. x)"
-  unfolding continuous_within Lim_within by auto
+  unfolding continuous_within by (rule Lim_at_within [OF Lim_ident_at])
 
 lemma continuous_at_id:
  "continuous (at a) (\<lambda>x. x)"
-  unfolding continuous_at Lim_at by auto
+  unfolding continuous_at by (rule Lim_ident_at)
 
 lemma continuous_on_id:
  "continuous_on s (\<lambda>x. x)"
@@ -3568,6 +3544,8 @@
 text{* Continuity of all kinds is preserved under composition. *}
 
 lemma continuous_within_compose:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
   assumes "continuous (at x within s) f"   "continuous (at (f x) within f ` s) g"
   shows "continuous (at x within s) (g o f)"
 proof-
@@ -3582,6 +3560,8 @@
 qed
 
 lemma continuous_at_compose:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
   assumes "continuous (at x) f"  "continuous (at (f x)) g"
   shows "continuous (at x) (g o f)"
 proof-
@@ -3607,7 +3587,8 @@
 text{* Continuity in terms of open preimages. *}
 
 lemma continuous_at_open:
- "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
 proof
   assume ?lhs
   { fix t assume as: "open t" "f x \<in> t"
@@ -3736,13 +3717,25 @@
 qed
 
 lemma continuous_open_preimage_univ:
-  "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
   using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
 
 lemma continuous_closed_preimage_univ:
-  "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
   using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
 
+lemma continuous_open_vimage:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
+  unfolding vimage_def by (rule continuous_open_preimage_univ)
+
+lemma continuous_closed_vimage:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+  shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
+  unfolding vimage_def by (rule continuous_closed_preimage_univ)
+
 text{* Equality of continuous functions on closure and related results.          *}
 
 lemma continuous_closed_in_preimage_constant:
@@ -3786,6 +3779,7 @@
 text{* Making a continuous function avoid some value in a neighbourhood.         *}
 
 lemma continuous_within_avoid:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   assumes "continuous (at x within s) f"  "x \<in> s"  "f x \<noteq> a"
   shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
 proof-
@@ -3798,6 +3792,7 @@
 qed
 
 lemma continuous_at_avoid:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   assumes "continuous (at x) f"  "f x \<noteq> a"
   shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
 using assms using continuous_within_avoid[of x UNIV f a, unfolded within_UNIV] by auto
@@ -3873,7 +3868,7 @@
 qed
 
 lemma open_affinity:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s"  "c \<noteq> 0"
   shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof-
@@ -4025,59 +4020,44 @@
 
 subsection{* Topological properties of linear functions.                               *}
 
-lemma linear_lim_0: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
-  assumes "linear f" shows "(f ---> 0) (at (0))"
+lemma linear_lim_0:
+  assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
 proof-
-  obtain B where "B>0" and B:"\<forall>x. norm (f x) \<le> B * norm x" using linear_bounded_pos[OF assms] by auto
-  { fix e::real assume "e>0"
-    { fix x::"real^'a" assume "norm x < e / B"
-      hence "B * norm x < e" using `B>0` using mult_strict_right_mono[of "norm x" " e / B" B] unfolding real_mult_commute by auto
-      hence "norm (f x) < e" using B[THEN spec[where x=x]] `B>0` using order_le_less_trans[of "norm (f x)" "B * norm x" e] by auto   }
-    moreover have "e / B > 0" using `e>0` `B>0` divide_pos_pos by auto
-    ultimately have "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f x) 0 < e" unfolding dist_norm by auto  }
-  thus ?thesis unfolding Lim_at by auto
-qed
-
-lemma bounded_linear_continuous_at:
+  interpret f: bounded_linear f by fact
+  have "(f ---> f 0) (at 0)"
+    using tendsto_ident_at by (rule f.tendsto)
+  thus ?thesis unfolding f.zero .
+qed
+
+lemma linear_continuous_at:
   assumes "bounded_linear f"  shows "continuous (at a) f"
   unfolding continuous_at using assms
   apply (rule bounded_linear.tendsto)
-  apply (rule Lim_at_id [unfolded id_def])
+  apply (rule tendsto_ident_at)
   done
 
-lemma linear_continuous_at:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
-  assumes "linear f"  shows "continuous (at a) f"
-  using assms unfolding linear_conv_bounded_linear
-  by (rule bounded_linear_continuous_at)
-
 lemma linear_continuous_within:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
-  shows "linear f ==> continuous (at x within s) f"
+  shows "bounded_linear f ==> continuous (at x within s) f"
   using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
 
 lemma linear_continuous_on:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
-  shows "linear f ==> continuous_on s f"
+  shows "bounded_linear f ==> continuous_on s f"
   using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
 
 text{* Also bilinear functions, in composition form.                             *}
 
 lemma bilinear_continuous_at_compose:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
-  shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
+  shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
         ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
   unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
 
 lemma bilinear_continuous_within_compose:
-  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
-  shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
+  shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
         ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
   unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
 
 lemma bilinear_continuous_on_compose:
-  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
-  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bilinear h
+  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
              ==> continuous_on s (\<lambda>x. h (f x) (g x))"
   unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
   using bilinear_continuous_within_compose[of _ s f g h] by auto
@@ -4233,10 +4213,10 @@
 subsection{* We can now extend limit compositions to consider the scalar multiplier.   *}
 
 lemma Lim_mul:
-  fixes f :: "'a \<Rightarrow> real ^ _"
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "(c ---> d) net"  "(f ---> l) net"
   shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
-  unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto)
+  using assms by (rule scaleR.tendsto)
 
 lemma Lim_vmul:
   fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
@@ -4367,25 +4347,20 @@
 
 text{* Hence some useful properties follow quite easily.                         *}
 
-lemma compact_scaleR_image:
+lemma compact_scaling:
   fixes s :: "'a::real_normed_vector set"
-  assumes "compact s"  shows "compact ((\<lambda>x. scaleR c x) ` s)"
+  assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
 proof-
   let ?f = "\<lambda>x. scaleR c x"
   have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
   show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
-    using bounded_linear_continuous_at[OF *] assms by auto
-qed
-
-lemma compact_scaling:
-  fixes s :: "(real ^ _) set"
-  assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
-  using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image)
+    using linear_continuous_at[OF *] assms by auto
+qed
 
 lemma compact_negations:
   fixes s :: "'a::real_normed_vector set"
   assumes "compact s"  shows "compact ((\<lambda>x. -x) ` s)"
-  using compact_scaleR_image [OF assms, of "- 1"] by auto
+  using compact_scaling [OF assms, of "- 1"] by auto
 
 lemma compact_sums:
   fixes s t :: "'a::real_normed_vector set"
@@ -4416,7 +4391,7 @@
 qed
 
 lemma compact_affinity:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
   assumes "compact s"  shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof-
   have "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
@@ -4490,9 +4465,9 @@
 
 text{* Related results with closure as the conclusion.                           *}
 
-lemma closed_scaleR_image:
+lemma closed_scaling:
   fixes s :: "'a::real_normed_vector set"
-  assumes "closed s" shows "closed ((\<lambda>x. scaleR c x) ` s)"
+  assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
 proof(cases "s={}")
   case True thus ?thesis by auto
 next
@@ -4524,15 +4499,10 @@
   qed
 qed
 
-lemma closed_scaling:
-  fixes s :: "(real ^ _) set"
-  assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
-  using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image)
-
 lemma closed_negations:
   fixes s :: "'a::real_normed_vector set"
   assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
-  using closed_scaleR_image[OF assms, of "- 1"] by simp
+  using closed_scaling[OF assms, of "- 1"] by simp
 
 lemma compact_closed_sums:
   fixes s :: "'a::real_normed_vector set"
@@ -5149,24 +5119,12 @@
 
 subsection{* Closure of halfspaces and hyperplanes.                                    *}
 
-lemma Lim_dot: fixes f :: "real^'m \<Rightarrow> real^'n::finite"
-  assumes "(f ---> l) net"  shows "((\<lambda>y. a \<bullet> (f y)) ---> a \<bullet> l) net"
-  unfolding dot_def by (intro tendsto_intros assms)
-
-lemma continuous_at_dot:
-  fixes x :: "real ^ _"
-  shows "continuous (at x) (\<lambda>y. a \<bullet> y)"
-proof-
-  have "((\<lambda>x. x) ---> x) (at x)" unfolding Lim_at by auto
-  thus ?thesis unfolding continuous_at and o_def using Lim_dot[of "\<lambda>x. x" x "at x" a] by auto
-qed
-
-lemma continuous_on_dot:
-  fixes s :: "(real ^ _) set"
-  shows "continuous_on s (\<lambda>y. a \<bullet> y)"
-  using continuous_at_imp_continuous_on[of s "\<lambda>y. a \<bullet> y"]
-  using continuous_at_dot
-  by auto
+lemma Lim_inner:
+  assumes "(f ---> l) net"  shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
+  by (intro tendsto_intros assms)
+
+lemma continuous_at_inner: "continuous (at x) (inner a)"
+  unfolding continuous_at by (intro tendsto_intros)
 
 lemma continuous_on_inner:
   fixes s :: "'a::real_inner set"
@@ -5175,16 +5133,12 @@
 
 lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
 proof-
-  have *:"{x \<in> UNIV. inner a x \<in> {r. \<exists>x. inner a x = r \<and> r \<le> b}} = {x. inner a x \<le> b}" by auto
-  let ?T = "{..b}"
-  have "closed ?T" by (rule closed_real_atMost)
-  moreover have "{r. \<exists>x. inner a x = r \<and> r \<le> b} = range (inner a) \<inter> ?T"
-    unfolding image_def by auto
-  ultimately have "\<exists>T. closed T \<and> {r. \<exists>x. inner a x = r \<and> r \<le> b} = range (inner a) \<inter> T" by fast
-  hence "closedin euclidean {x \<in> UNIV. inner a x \<in> {r. \<exists>x. inner a x = r \<and> r \<le> b}}"
-    using continuous_on_inner[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed
-    by (fast elim!: allE[where x="{r. (\<exists>x. inner a x = r \<and> r \<le> b)}"])
-  thus ?thesis unfolding closed_closedin[THEN sym] and * by auto
+  have "\<forall>x. continuous (at x) (inner a)"
+    unfolding continuous_at by (rule allI) (intro tendsto_intros)
+  hence "closed (inner a -` {..b})"
+    using closed_real_atMost by (rule continuous_closed_vimage)
+  moreover have "{x. inner a x \<le> b} = inner a -` {..b}" by auto
+  ultimately show ?thesis by simp
 qed
 
 lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
@@ -5279,7 +5233,7 @@
   using assms unfolding continuous_on unfolding Lim_within_union
   unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto
 
-lemma continuous_on_cases: fixes g :: "real^'m::finite \<Rightarrow> real ^'n::finite"
+lemma continuous_on_cases:
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
           "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
   shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
@@ -5335,22 +5289,24 @@
      (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
      (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
 
-definition homeomorphic :: "((real^'a::finite) set) \<Rightarrow> ((real^'b::finite) set) \<Rightarrow> bool" (infixr "homeomorphic" 60) where
+definition
+  homeomorphic :: "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> bool"
+    (infixr "homeomorphic" 60) where
   homeomorphic_def: "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
 
 lemma homeomorphic_refl: "s homeomorphic s"
   unfolding homeomorphic_def
   unfolding homeomorphism_def
   using continuous_on_id
-  apply(rule_tac x = "(\<lambda>x::real^'a.x)" in exI)
-  apply(rule_tac x = "(\<lambda>x::real^'b.x)" in exI)
+  apply(rule_tac x = "(\<lambda>x. x)" in exI)
+  apply(rule_tac x = "(\<lambda>x. x)" in exI)
   by blast
 
 lemma homeomorphic_sym:
  "s homeomorphic t \<longleftrightarrow> t homeomorphic s"
 unfolding homeomorphic_def
 unfolding homeomorphism_def
-by blast
+by blast (* FIXME: slow *)
 
 lemma homeomorphic_trans:
   assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u"
@@ -5392,7 +5348,8 @@
  using assms unfolding inj_on_def inv_on_def by auto
 
 lemma homeomorphism_compact:
-  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+    (* class constraint due to continuous_on_inverse *)
   assumes "compact s" "continuous_on s f"  "f ` s = t"  "inj_on f s"
   shows "\<exists>g. homeomorphism s t f g"
 proof-
@@ -5419,7 +5376,9 @@
 qed
 
 lemma homeomorphic_compact:
- "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+    (* class constraint due to continuous_on_inverse *)
+  shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
           \<Longrightarrow> s homeomorphic t"
   unfolding homeomorphic_def by(metis homeomorphism_compact)
 
@@ -5433,6 +5392,7 @@
 text{* Results on translation, scaling etc.                                      *}
 
 lemma homeomorphic_scaling:
+  fixes s :: "'a::real_normed_vector set"
   assumes "c \<noteq> 0"  shows "s homeomorphic ((\<lambda>x. c *\<^sub>R x) ` s)"
   unfolding homeomorphic_minimal
   apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
@@ -5441,13 +5401,15 @@
   using continuous_on_cmul[OF continuous_on_id] by auto
 
 lemma homeomorphic_translation:
- "s homeomorphic ((\<lambda>x. a + x) ` s)"
+  fixes s :: "'a::real_normed_vector set"
+  shows "s homeomorphic ((\<lambda>x. a + x) ` s)"
   unfolding homeomorphic_minimal
   apply(rule_tac x="\<lambda>x. a + x" in exI)
   apply(rule_tac x="\<lambda>x. -a + x" in exI)
   using continuous_on_add[OF continuous_on_const continuous_on_id] by auto
 
 lemma homeomorphic_affinity:
+  fixes s :: "'a::real_normed_vector set"
   assumes "c \<noteq> 0"  shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof-
   have *:"op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
@@ -5457,7 +5419,8 @@
     using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a] unfolding * by auto
 qed
 
-lemma homeomorphic_balls: fixes a b ::"real^'a::finite"
+lemma homeomorphic_balls:
+  fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *)
   assumes "0 < d"  "0 < e"
   shows "(ball a d) homeomorphic  (ball b e)" (is ?th)
         "(cball a d) homeomorphic (cball b e)" (is ?cth)
@@ -5487,14 +5450,15 @@
 
 lemma cauchy_isometric:
   fixes x :: "nat \<Rightarrow> real ^ 'n::finite"
-  assumes e:"0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
+  assumes e:"0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
   shows "Cauchy x"
 proof-
+  interpret f: bounded_linear f by fact
   { fix d::real assume "d>0"
     then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
       using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
     { fix n assume "n\<ge>N"
-      hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding linear_sub[OF f, THEN sym] by auto
+      hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding f.diff[THEN sym] by auto
       moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
 	using subspace_sub[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
 	using normf[THEN bspec[where x="x n - x N"]] by auto
@@ -5506,7 +5470,7 @@
 
 lemma complete_isometric_image:
   fixes f :: "real ^ _ \<Rightarrow> real ^ _"
-  assumes "0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
+  assumes "0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
   shows "complete(f ` s)"
 proof-
   { fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g"
@@ -5529,7 +5493,7 @@
 unfolding dist_norm by simp
 
 lemma injective_imp_isometric: fixes f::"real^'m::finite \<Rightarrow> real^'n::finite"
-  assumes s:"closed s"  "subspace s"  and f:"linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
+  assumes s:"closed s"  "subspace s"  and f:"bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
   shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm(x)"
 proof(cases "s \<subseteq> {0::real^'m}")
   case True
@@ -5538,6 +5502,7 @@
     hence "norm x \<le> norm (f x)" by auto  }
   thus ?thesis by(auto intro!: exI[where x=1])
 next
+  interpret f: bounded_linear f by fact
   case False
   then obtain a where a:"a\<noteq>0" "a\<in>s" by auto
   from False have "s \<noteq> {}" by auto
@@ -5571,7 +5536,7 @@
       have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s" using s[unfolded subspace_def smult_conv_scaleR] by auto
       hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}" using `x\<in>s` and `x\<noteq>0` by auto
       thus "norm (f b) / norm b * norm x \<le> norm (f x)" using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
-	unfolding linear_cmul[OF f(1), unfolded smult_conv_scaleR] and ba using `x\<noteq>0` `a\<noteq>0`
+	unfolding f.scaleR and ba using `x\<noteq>0` `a\<noteq>0`
 	by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq)
     qed }
   ultimately
@@ -5579,8 +5544,8 @@
 qed
 
 lemma closed_injective_image_subspace:
-  fixes s :: "(real ^ _) set"
-  assumes "subspace s" "linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
   shows "closed(f ` s)"
 proof-
   obtain e where "e>0" and e:"\<forall>x\<in>s. e * norm x \<le> norm (f x)" using injective_imp_isometric[OF assms(4,1,2,3)] by auto
@@ -5688,10 +5653,11 @@
   then obtain d::"'n set" where t: "card d = dim s"
     using closed_subspace_lemma by auto
   let ?t = "{x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0}"
-  obtain f where f:"linear f"  "f ` ?t = s" "inj_on f ?t"
-    using subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"] assms]
+  obtain f where f:"bounded_linear f"  "f ` ?t = s" "inj_on f ?t"
+    using subspace_isomorphism[unfolded linear_conv_bounded_linear, OF subspace_substandard[of "\<lambda>i. i \<notin> d"] assms]
     using dim_substandard[of d] and t by auto
-  have "\<forall>x\<in>?t. f x = 0 \<longrightarrow> x = 0" using linear_0[OF f(1)] using f(3)[unfolded inj_on_def]
+  interpret f: bounded_linear f by fact
+  have "\<forall>x\<in>?t. f x = 0 \<longrightarrow> x = 0" using f.zero using f(3)[unfolded inj_on_def]
     by(erule_tac x=0 in ballE) auto
   moreover have "closed ?t" using closed_substandard .
   moreover have "subspace ?t" using subspace_substandard .

--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -101,8 +101,9 @@
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
           let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
-              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
-              val inject_flat = Library.flat inject
+              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype
+                DatatypeAux.default_datatype_config [ak] [dt] thy
+              val inject_flat = flat inject
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
               

--- a/src/HOL/Nominal/nominal_package.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -6,8 +6,9 @@
 
 signature NOMINAL_PACKAGE =
 sig
-  val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix *
-    (bstring * string list * mixfix) list) list -> theory -> theory
+  val add_nominal_datatype : DatatypeAux.datatype_config -> string list ->
+    (string list * bstring * mixfix *
+      (bstring * string list * mixfix) list) list -> theory -> theory
   type descr
   type nominal_datatype_info
   val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
@@ -190,7 +191,7 @@
 fun fresh_star_const T U =
   Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
 
-fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
+fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
   let
     (* this theory is used just for parsing *)
 
@@ -243,7 +244,7 @@
     val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
 
     val ({induction, ...},thy1) =
-      DatatypePackage.add_datatype err flat_names new_type_names' dts'' thy;
+      DatatypePackage.add_datatype config new_type_names' dts'' thy;
 
     val SOME {descr, ...} = Symtab.lookup
       (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
@@ -815,7 +816,7 @@
         val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
           ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
       in
-        (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
+        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
       end;
 
     val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
@@ -1509,7 +1510,7 @@
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10 |>
         InductivePackage.add_inductive_global (serial_string ())
-          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
@@ -2067,7 +2068,7 @@
     thy13
   end;
 
-val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ true;
+val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ;
 
 
 (* FIXME: The following stuff should be exported by DatatypePackage *)
@@ -2083,7 +2084,7 @@
     val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
     val specs = map (fn ((((_, vs), t), mx), cons) =>
       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
-  in add_nominal_datatype false names specs end;
+  in add_nominal_datatype DatatypeAux.default_datatype_config names specs end;
 
 val _ =
   OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl

--- a/src/HOL/Product_Type.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Product_Type.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)

--- a/src/HOL/Quickcheck.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Quickcheck.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -137,7 +137,7 @@
 code_reserved Quickcheck Quickcheck_Generators
 
 
-hide (open) const collapse beyond random_fun_aux random_fun_lift
+hide (open) const random collapse beyond random_fun_aux random_fun_lift
 
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)

--- a/src/HOL/Rational.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Rational.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -1012,7 +1012,7 @@
 begin
 
 definition
-  "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
+  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
      let j = Code_Numeral.int_of (denom + 1)
      in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
 
@@ -1048,7 +1048,7 @@
     val p' = p div g;
     val q' = q div g;
     val r = (if one_of [true, false] then p' else ~ p',
-      if p' = 0 then 0 else q')
+      if p' = 0 then 1 else q')
   in
     (r, fn () => term_of_rat r)
   end;
@@ -1060,8 +1060,7 @@
 consts_code
   "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
 attach {*
-fun rat_of_int 0 = (0, 0)
-  | rat_of_int i = (i, 1);
+fun rat_of_int i = (i, 1);
 *}
 
 end

--- a/src/HOL/RealDef.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/RealDef.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -1137,7 +1137,7 @@
 begin
 
 definition
-  "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
 
 instance ..
 
@@ -1169,7 +1169,7 @@
     val p' = p div g;
     val q' = q div g;
     val r = (if one_of [true, false] then p' else ~ p',
-      if p' = 0 then 0 else q')
+      if p' = 0 then 1 else q')
   in
     (r, fn () => term_of_real r)
   end;
@@ -1181,8 +1181,7 @@
 consts_code
   "of_int :: int \<Rightarrow> real" ("\<module>real'_of'_int")
 attach {*
-fun real_of_int 0 = (0, 0)
-  | real_of_int i = (i, 1);
+fun real_of_int i = (i, 1);
 *}
 
 end

--- a/src/HOL/Set.thy	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Set.thy	Wed Jun 17 10:08:06 2009 +0200
@@ -23,8 +23,6 @@
   Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
   Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
   Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
-  Pow           :: "'a set => 'a set set"                -- "powerset"
-  image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
 
 local
 
@@ -215,9 +213,6 @@
   supset_eq  ("op \<supseteq>") and
   supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
 
-abbreviation
-  range :: "('a => 'b) => 'b set" where -- "of function"
-  "range f == f ` UNIV"
 
 
 subsubsection "Bounded quantifiers"
@@ -408,9 +403,15 @@
 
 end
 
-defs
-  Pow_def:      "Pow A          == {B. B <= A}"
-  image_def:    "f`A            == {y. EX x:A. y = f(x)}"
+definition Pow :: "'a set => 'a set set" where
+  Pow_def: "Pow A = {B. B \<le> A}"
+
+definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
+  image_def: "f ` A = {y. EX x:A. y = f(x)}"
+
+abbreviation
+  range :: "('a => 'b) => 'b set" where -- "of function"
+  "range f == f ` UNIV"
 
 
 subsection {* Lemmas and proof tool setup *}

--- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -14,26 +14,29 @@
 
 signature DATATYPE_ABS_PROOFS =
 sig
-  val prove_casedist_thms : string list ->
-    DatatypeAux.descr list -> (string * sort) list -> thm ->
+  type datatype_config = DatatypeAux.datatype_config
+  type descr = DatatypeAux.descr
+  type datatype_info = DatatypeAux.datatype_info
+  val prove_casedist_thms : datatype_config -> string list ->
+    descr list -> (string * sort) list -> thm ->
     attribute list -> theory -> thm list * theory
-  val prove_primrec_thms : bool -> string list ->
-    DatatypeAux.descr list -> (string * sort) list ->
-      DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
+  val prove_primrec_thms : datatype_config -> string list ->
+    descr list -> (string * sort) list ->
+      datatype_info Symtab.table -> thm list list -> thm list list ->
         simpset -> thm -> theory -> (string list * thm list) * theory
-  val prove_case_thms : bool -> string list ->
-    DatatypeAux.descr list -> (string * sort) list ->
+  val prove_case_thms : datatype_config -> string list ->
+    descr list -> (string * sort) list ->
       string list -> thm list -> theory -> (thm list list * string list) * theory
-  val prove_split_thms : string list ->
-    DatatypeAux.descr list -> (string * sort) list ->
+  val prove_split_thms : datatype_config -> string list ->
+    descr list -> (string * sort) list ->
       thm list list -> thm list list -> thm list -> thm list list -> theory ->
         (thm * thm) list * theory
-  val prove_nchotomys : string list -> DatatypeAux.descr list ->
+  val prove_nchotomys : datatype_config -> string list -> descr list ->
     (string * sort) list -> thm list -> theory -> thm list * theory
-  val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
+  val prove_weak_case_congs : string list -> descr list ->
     (string * sort) list -> theory -> thm list * theory
   val prove_case_congs : string list ->
-    DatatypeAux.descr list -> (string * sort) list ->
+    descr list -> (string * sort) list ->
       thm list -> thm list list -> theory -> thm list * theory
 end;
 
@@ -44,9 +47,9 @@
 
 (************************ case distinction theorems ***************************)
 
-fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
+fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
   let
-    val _ = message "Proving case distinction theorems ...";
+    val _ = message config "Proving case distinction theorems ...";
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
@@ -86,13 +89,13 @@
 
 (*************************** primrec combinators ******************************)
 
-fun prove_primrec_thms flat_names new_type_names descr sorts
+fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
     (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
   let
-    val _ = message "Constructing primrec combinators ...";
+    val _ = message config "Constructing primrec combinators ...";
 
     val big_name = space_implode "_" new_type_names;
-    val thy0 = add_path flat_names big_name thy;
+    val thy0 = add_path (#flat_names config) big_name thy;
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
@@ -153,7 +156,7 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
         InductivePackage.add_inductive_global (serial_string ())
-          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
             alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
             skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
@@ -162,7 +165,7 @@
 
     (* prove uniqueness and termination of primrec combinators *)
 
-    val _ = message "Proving termination and uniqueness of primrec functions ...";
+    val _ = message config "Proving termination and uniqueness of primrec functions ...";
 
     fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
       let
@@ -242,13 +245,13 @@
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
-      ||> parent_path flat_names
+      ||> parent_path (#flat_names config) 
       ||> Theory.checkpoint;
 
 
     (* prove characteristic equations for primrec combinators *)
 
-    val _ = message "Proving characteristic theorems for primrec combinators ..."
+    val _ = message config "Proving characteristic theorems for primrec combinators ..."
 
     val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
       (fn _ => EVERY
@@ -272,11 +275,11 @@
 
 (***************************** case combinators *******************************)
 
-fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
   let
-    val _ = message "Proving characteristic theorems for case combinators ...";
+    val _ = message config "Proving characteristic theorems for case combinators ...";
 
-    val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
+    val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
@@ -338,7 +341,7 @@
     thy2
     |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
        o Context.Theory
-    |> parent_path flat_names
+    |> parent_path (#flat_names config)
     |> store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
   end;
@@ -346,12 +349,12 @@
 
 (******************************* case splitting *******************************)
 
-fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
+fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
     casedist_thms case_thms thy =
   let
-    val _ = message "Proving equations for case splitting ...";
+    val _ = message config "Proving equations for case splitting ...";
 
-    val descr' = List.concat descr;
+    val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val newTs = Library.take (length (hd descr), recTs);
 
@@ -395,9 +398,9 @@
 
 (************************* additional theorems for TFL ************************)
 
-fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
   let
-    val _ = message "Proving additional theorems for TFL ...";
+    val _ = message config "Proving additional theorems for TFL ...";
 
     fun prove_nchotomy (t, exhaustion) =
       let

--- a/src/HOL/Tools/datatype_package/datatype_aux.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_aux.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -6,8 +6,9 @@
 
 signature DATATYPE_AUX =
 sig
-  val quiet_mode : bool ref
-  val message : string -> unit
+  type datatype_config
+  val default_datatype_config : datatype_config
+  val message : datatype_config -> string -> unit
   
   val add_path : bool -> string -> theory -> theory
   val parent_path : bool -> theory -> theory
@@ -67,8 +68,13 @@
 structure DatatypeAux : DATATYPE_AUX =
 struct
 
-val quiet_mode = ref false;
-fun message s = if !quiet_mode then () else writeln s;
+(* datatype option flags *)
+
+type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
+val default_datatype_config : datatype_config =
+  { strict = true, flat_names = false, quiet = false };
+fun message ({ quiet, ...} : datatype_config) s =
+  if quiet then () else writeln s;
 
 fun add_path flat_names s = if flat_names then I else Sign.add_path s;
 fun parent_path flat_names = if flat_names then I else Sign.parent_path;

--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -426,7 +426,7 @@
 
 (* register a datatype etc. *)
 
-fun add_all_code dtcos thy =
+fun add_all_code config dtcos thy =
   let
     val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
     val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
@@ -437,7 +437,7 @@
   in
     if null css then thy
     else thy
-      |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...")
+      |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...")
       |> fold Code.add_datatype css
       |> fold_rev Code.add_default_eqn case_rewrites
       |> fold Code.add_case certs

--- a/src/HOL/Tools/datatype_package/datatype_package.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_package.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -6,6 +6,7 @@
 
 signature DATATYPE_PACKAGE =
 sig
+  type datatype_config = DatatypeAux.datatype_config
   type datatype_info = DatatypeAux.datatype_info
   type descr = DatatypeAux.descr
   val get_datatypes : theory -> datatype_info Symtab.table
@@ -24,39 +25,23 @@
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
   val read_typ: theory ->
     (typ list * (string * sort) list) * string -> typ list * (string * sort) list
-  val interpretation : (string list -> theory -> theory) -> theory -> theory
-  val rep_datatype : ({distinct : thm list list,
-       inject : thm list list,
-       exhaustion : thm list,
-       rec_thms : thm list,
-       case_thms : thm list list,
-       split_thms : (thm * thm) list,
-       induction : thm,
-       simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
-    -> theory -> Proof.state;
-  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
-  val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
-    (binding * typ list * mixfix) list) list -> theory ->
-      {distinct : thm list list,
-       inject : thm list list,
-       exhaustion : thm list,
-       rec_thms : thm list,
-       case_thms : thm list list,
-       split_thms : (thm * thm) list,
-       induction : thm,
-       simps : thm list} * theory
-  val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
-    (binding * string list * mixfix) list) list -> theory ->
-      {distinct : thm list list,
-       inject : thm list list,
-       exhaustion : thm list,
-       rec_thms : thm list,
-       case_thms : thm list list,
-       split_thms : (thm * thm) list,
-       induction : thm,
-       simps : thm list} * theory
+  val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
+  type rules = {distinct : thm list list,
+    inject : thm list list,
+    exhaustion : thm list,
+    rec_thms : thm list,
+    case_thms : thm list list,
+    split_thms : (thm * thm) list,
+    induction : thm,
+    simps : thm list}
+  val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
+    -> string list option -> term list -> theory -> Proof.state;
+  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
+  val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
+    (binding * typ list * mixfix) list) list -> theory -> rules * theory
+  val add_datatype_cmd : string list -> (string list * binding * mixfix *
+    (binding * string list * mixfix) list) list -> theory -> rules * theory
   val setup: theory -> theory
-  val quiet_mode : bool ref
   val print_datatypes : theory -> unit
 end;
 
@@ -65,8 +50,6 @@
 
 open DatatypeAux;
 
-val quiet_mode = quiet_mode;
-
 
 (* theory data *)
 
@@ -358,31 +341,41 @@
     case_cong = case_cong,
     weak_case_cong = weak_case_cong});
 
-structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
-val interpretation = DatatypeInterpretation.interpretation;
+type rules = {distinct : thm list list,
+  inject : thm list list,
+  exhaustion : thm list,
+  rec_thms : thm list,
+  case_thms : thm list list,
+  split_thms : (thm * thm) list,
+  induction : thm,
+  simps : thm list}
+
+structure DatatypeInterpretation = InterpretationFun
+  (type T = datatype_config * string list val eq = eq_snd op =);
+fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
 
 
 (******************* definitional introduction of datatypes *******************)
 
-fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
     case_names_induct case_names_exhausts thy =
   let
-    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
 
     val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
-      DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
+      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
         types_syntax constr_syntax case_names_induct;
 
-    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
+    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
       sorts induct case_names_exhausts thy2;
     val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
-      flat_names new_type_names descr sorts dt_info inject dist_rewrites
+      config new_type_names descr sorts dt_info inject dist_rewrites
       (Simplifier.theory_context thy3 dist_ss) induct thy3;
     val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
-      flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
-    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
+      config new_type_names descr sorts reccomb_names rec_thms thy4;
+    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
       descr sorts inject dist_rewrites casedist_thms case_thms thy6;
-    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
+    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
       descr sorts casedist_thms thy7;
     val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
       descr sorts nchotomys case_thms thy8;
@@ -406,7 +399,7 @@
       |> add_cases_induct dt_infos induct
       |> Sign.parent_path
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
-      |> DatatypeInterpretation.data (map fst dt_infos);
+      |> DatatypeInterpretation.data (config, map fst dt_infos);
   in
     ({distinct = distinct,
       inject = inject,
@@ -421,7 +414,7 @@
 
 (*********************** declare existing type as datatype *********************)
 
-fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy =
+fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
   let
     val ((_, [induct']), _) =
       Variable.importT_thms [induct] (Variable.thm_context induct);
@@ -440,19 +433,19 @@
     val (case_names_induct, case_names_exhausts) =
       (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
 
-    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
 
     val (casedist_thms, thy2) = thy |>
-      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
+      DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
         case_names_exhausts;
     val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
-      false new_type_names [descr] sorts dt_info inject distinct
+      config new_type_names [descr] sorts dt_info inject distinct
       (Simplifier.theory_context thy2 dist_ss) induct thy2;
-    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
-      new_type_names [descr] sorts reccomb_names rec_thms thy3;
+    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
+      config new_type_names [descr] sorts reccomb_names rec_thms thy3;
     val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
-      new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
-    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
+      config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
+    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names
       [descr] sorts casedist_thms thy5;
     val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
       [descr] sorts nchotomys case_thms thy6;
@@ -482,7 +475,7 @@
       |> Sign.parent_path
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
       |> snd
-      |> DatatypeInterpretation.data (map fst dt_infos);
+      |> DatatypeInterpretation.data (config, map fst dt_infos);
   in
     ({distinct = distinct,
       inject = inject,
@@ -494,7 +487,7 @@
       simps = simps}, thy11)
   end;
 
-fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
+fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
   let
     fun constr_of_term (Const (c, T)) = (c, T)
       | constr_of_term t =
@@ -550,7 +543,7 @@
             (*FIXME somehow dubious*)
       in
         ProofContext.theory_result
-          (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts)
+          (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
         #-> after_qed
       end;
   in
@@ -560,13 +553,13 @@
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
 
 
 
 (******************************** add datatype ********************************)
 
-fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
+fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
   let
     val _ = Theory.requires thy "Datatype" "datatype definitions";
 
@@ -598,7 +591,7 @@
             val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs))
-          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
+          in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else
                 Sign.full_name_path tmp_thy tname')
                   (Binding.map_name (Syntax.const_name mx') cname),
                    map (dtyp_of_typ new_dts) cargs')],
@@ -626,7 +619,7 @@
     val dt_info = get_datatypes thy;
     val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
     val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
-      if err then error ("Nonemptiness check failed for datatype " ^ s)
+      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
       else raise exn;
 
     val descr' = flat descr;
@@ -634,12 +627,12 @@
     val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   in
     add_datatype_def
-      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+      (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
       case_names_induct case_names_exhausts thy
   end;
 
 val add_datatype = gen_add_datatype cert_typ;
-val add_datatype_cmd = gen_add_datatype read_typ true;
+val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
 
 
 
@@ -668,7 +661,7 @@
       (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
     val specs = map (fn ((((_, vs), t), mx), cons) =>
       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
-  in snd o add_datatype_cmd false names specs end;
+  in snd o add_datatype_cmd names specs end;
 
 val _ =
   OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl

--- a/src/HOL/Tools/datatype_package/datatype_realizer.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -7,7 +7,7 @@
 
 signature DATATYPE_REALIZER =
 sig
-  val add_dt_realizers: string list -> theory -> theory
+  val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
   val setup: theory -> theory
 end;
 
@@ -213,10 +213,10 @@
      (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
   end;
 
-fun add_dt_realizers names thy =
+fun add_dt_realizers config names thy =
   if ! Proofterm.proofs < 2 then thy
   else let
-    val _ = message "Adding realizers for induction and case analysis ..."
+    val _ = message config "Adding realizers for induction and case analysis ..."
     val infos = map (DatatypePackage.the_datatype thy) names;
     val info :: _ = infos;
   in

--- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -11,10 +11,13 @@
 
 signature DATATYPE_REP_PROOFS =
 sig
+  type datatype_config = DatatypeAux.datatype_config
+  type descr = DatatypeAux.descr
+  type datatype_info = DatatypeAux.datatype_info
   val distinctness_limit : int Config.T
   val distinctness_limit_setup : theory -> theory
-  val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
-    string list -> DatatypeAux.descr list -> (string * sort) list ->
+  val representation_proofs : datatype_config -> datatype_info Symtab.table ->
+    string list -> descr list -> (string * sort) list ->
       (binding * mixfix) list -> (binding * mixfix) list list -> attribute
         -> theory -> (thm list list * thm list list * thm list list *
           DatatypeAux.simproc_dist list * thm) * theory
@@ -45,7 +48,7 @@
 
 (******************************************************************************)
 
-fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
+fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
     val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
@@ -69,7 +72,7 @@
     val descr' = flat descr;
 
     val big_name = space_implode "_" new_type_names;
-    val thy1 = add_path flat_names big_name thy;
+    val thy1 = add_path (#flat_names config) big_name thy;
     val big_rec_name = big_name ^ "_rep_set";
     val rep_set_names' =
       (if length descr' = 1 then [big_rec_name] else
@@ -147,7 +150,7 @@
 
     (************** generate introduction rules for representing set **********)
 
-    val _ = message "Constructing representing sets ...";
+    val _ = message config "Constructing representing sets ...";
 
     (* make introduction rule for a single constructor *)
 
@@ -181,7 +184,7 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
         InductivePackage.add_inductive_global (serial_string ())
-          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
@@ -190,7 +193,7 @@
     (********************************* typedef ********************************)
 
     val (typedefs, thy3) = thy2 |>
-      parent_path flat_names |>
+      parent_path (#flat_names config) |>
       fold_map (fn ((((name, mx), tvs), c), name') =>
           TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
@@ -199,7 +202,7 @@
               (resolve_tac rep_intrs 1)))
                 (types_syntax ~~ tyvars ~~
                   (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
-      add_path flat_names big_name;
+      add_path (#flat_names config) big_name;
 
     (*********************** definition of constructors ***********************)
 
@@ -257,19 +260,19 @@
         val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
         val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
         val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
-          ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
+          ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax)
       in
-        (parent_path flat_names thy', defs', eqns @ [eqns'],
+        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'],
           rep_congs @ [cong'], dist_lemmas @ [dist])
       end;
 
     val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
-      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
+      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []),
         hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
 
     (*********** isomorphisms for new types (introduced by typedef) ***********)
 
-    val _ = message "Proving isomorphism properties ...";
+    val _ = message config "Proving isomorphism properties ...";
 
     val newT_iso_axms = map (fn (_, td) =>
       (collect_simp (#Abs_inverse td), #Rep_inverse td,
@@ -358,7 +361,7 @@
       in (thy', char_thms' @ char_thms) end;
 
     val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
-      (add_path flat_names big_name thy4, []) (tl descr));
+      (add_path (#flat_names config) big_name thy4, []) (tl descr));
 
     (* prove isomorphism properties *)
 
@@ -458,9 +461,9 @@
       let val isoT = T --> Univ_elT
       in HOLogic.imp $ 
         (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
-          (if i < length newTs then Const ("True", HOLogic.boolT)
+          (if i < length newTs then HOLogic.true_const
            else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
-             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
+             Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
                Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
       end;
 
@@ -496,7 +499,7 @@
 
     (******************* freeness theorems for constructors *******************)
 
-    val _ = message "Proving freeness of constructors ...";
+    val _ = message config "Proving freeness of constructors ...";
 
     (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
     
@@ -568,13 +571,13 @@
 
     val ((constr_inject', distinct_thms'), thy6) =
       thy5
-      |> parent_path flat_names
+      |> parent_path (#flat_names config)
       |> store_thmss "inject" new_type_names constr_inject
       ||>> store_thmss "distinct" new_type_names distinct_thms;
 
     (*************************** induction theorem ****************************)
 
-    val _ = message "Proving induction rule for datatypes ...";
+    val _ = message config "Proving induction rule for datatypes ...";
 
     val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
       (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);

--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -191,9 +191,7 @@
                            |> safe_mk_meta_eq)))
                        thy
 
-val case_cong = fold add_case_cong
-
-val setup_case_cong = DatatypePackage.interpretation case_cong
+val setup_case_cong = DatatypePackage.interpretation (K (fold add_case_cong))
 
 
 (* setup *)

--- a/src/HOL/Tools/function_package/size.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -218,7 +218,7 @@
       (new_type_names ~~ size_names)) thy''
   end;
 
-fun add_size_thms (new_type_names as name :: _) thy =
+fun add_size_thms config (new_type_names as name :: _) thy =
   let
     val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
     val prefix = Long_Name.map_base_name (K (space_implode "_"

--- a/src/HOL/Tools/inductive_realizer.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -307,8 +307,8 @@
 
     val ((dummies, dt_info), thy2) =
       thy1
-      |> add_dummies
-           (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
+      |> add_dummies (DatatypePackage.add_datatype
+           { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
            (map (pair false) dts) []
       ||> Extraction.add_typeof_eqns_i ty_eqs
       ||> Extraction.add_realizes_eqns_i rlz_eqs;

--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -15,7 +15,7 @@
   val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
     -> string list -> string list * string list -> typ list * typ list
     -> string * (term list * (term * term) list)
-  val ensure_random_datatype: string list -> theory -> theory
+  val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
   val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
   val setup: theory -> theory
 end;
@@ -49,7 +49,7 @@
       mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
         (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit => term"}, t')));
     fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
-      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
+      (Sign.mk_const thy (@{const_name Quickcheck.random}, [ty]) $ Bound i);
   in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
 
 fun compile_generator_expr thy t =
@@ -98,7 +98,7 @@
     val Ttm = mk_termifyT T;
     val typtm = mk_termifyT typ;
     fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
-    fun mk_random T = mk_const @{const_name random} [T];
+    fun mk_random T = mk_const @{const_name Quickcheck.random} [T];
     val size = @{term "j::code_numeral"};
     val v = "x";
     val t_v = Free (v, typtm);
@@ -212,7 +212,7 @@
         fun prove_eqs aux_simp proj_defs lthy = 
           let
             val proj_simps = map (snd o snd) proj_defs;
-            fun tac { context = ctxt, ... } =
+            fun tac { context = ctxt, prems = _ } =
               ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
               THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
               THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
@@ -320,9 +320,9 @@
     val prefix = space_implode "_" (random_auxN :: names);
   in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
 
-fun mk_random_datatype descr vs tycos (names, auxnames) (Ts, Us) thy =
+fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
   let
-    val _ = DatatypeAux.message "Creating quickcheck generators ...";
+    val _ = DatatypeAux.message config "Creating quickcheck generators ...";
     val i = @{term "i\<Colon>code_numeral"};
     val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
@@ -356,7 +356,7 @@
   in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
   end handle CLASS_ERROR => NONE;
 
-fun ensure_random_datatype raw_tycos thy =
+fun ensure_random_datatype config raw_tycos thy =
   let
     val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy;
@@ -370,7 +370,7 @@
       can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
   in if has_inst then thy
     else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
-     of SOME constrain => mk_random_datatype descr
+     of SOME constrain => mk_random_datatype config descr
           (map constrain raw_vs) tycos (names, auxnames)
             ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
       | NONE => thy

--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -122,7 +122,7 @@
 
   val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
                lessD = [], neqE = [], simpset = Simplifier.empty_ss,
-               number_of = (serial (), no_number_of) };
+               number_of = (serial (), no_number_of) } : T;
   val extend = I;
   fun merge _
     ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,

--- a/src/Pure/Concurrent/future.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -301,19 +301,10 @@
       val _ = scheduler_check "join check";
       val _ = Multithreading.self_critical () andalso
         error "Cannot join future values within critical section";
-
       val _ =
-        (case thread_data () of
-          NONE => List.app join_wait xs  (*alien thread -- refrain from contending for resources*)
-        | SOME (name, task) =>           (*proper task -- continue work*)
-            let
-              val pending = filter_out is_finished xs;
-              val deps = map task_of pending;
-              val _ = SYNCHRONIZED "join" (fn () =>
-                (change queue (Task_Queue.depend deps task); notify_all ()));
-              val _ = List.app join_loop pending;
-            in () end);
-
+        if is_some (thread_data ())
+        then List.app join_loop xs   (*proper task -- continue work*)
+        else List.app join_wait xs;  (*alien thread -- refrain from contending for resources*)
     in map get_result xs end) ();
 
 end;

--- a/src/Pure/Concurrent/task_queue.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -21,7 +21,6 @@
   val is_empty: queue -> bool
   val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
-  val depend: task list -> task -> queue -> queue
   val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
   val interrupt: queue -> task -> unit
   val interrupt_external: queue -> string -> unit
@@ -74,9 +73,6 @@
 fun add_job task dep (jobs: jobs) =
   Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
 
-fun add_job_acyclic task dep (jobs: jobs) =
-  Task_Graph.add_edge_acyclic (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
-
 
 (* queue of grouped jobs *)
 
@@ -95,22 +91,25 @@
 
 (* enqueue *)
 
-fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, ...}) =
+fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, cache}) =
   let
     val task = new_task pri;
     val groups' = Inttab.cons_list (gid, task) groups;
     val jobs' = jobs
       |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps;
-  in (task, make_queue groups' jobs' Unknown) end;
+    val cache' =
+      (case cache of
+        Result last =>
+          if task_ord (last, task) = LESS
+          then cache else Unknown
+      | _ => Unknown);
+  in (task, make_queue groups' jobs' cache') end;
 
 fun extend task job (Queue {groups, jobs, cache}) =
   (case try (get_job jobs) task of
     SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) cache)
   | _ => NONE);
 
-fun depend deps task (Queue {groups, jobs, ...}) =
-  make_queue groups (fold (add_job_acyclic task) deps jobs) Unknown;
-
 
 (* dequeue *)
 
@@ -168,11 +167,14 @@
     val _ = List.app SimpleThread.interrupt running;
   in groups end;
 
-fun finish task (Queue {groups, jobs, ...}) =
+fun finish task (Queue {groups, jobs, cache}) =
   let
     val Group (gid, _) = get_group jobs task;
     val groups' = Inttab.remove_list (op =) (gid, task) groups;
     val jobs' = Task_Graph.del_node task jobs;
-  in make_queue groups' jobs' Unknown end;
+    val cache' =
+      if null (Task_Graph.imm_succs jobs task) then cache
+      else Unknown;
+  in make_queue groups' jobs' cache' end;
 
 end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/scan.scala	Wed Jun 17 10:08:06 2009 +0200
@@ -0,0 +1,140 @@
+/*  Title:      Pure/General/scan.scala
+    Author:     Makarius
+
+Efficient scanning of keywords.
+*/
+
+package isabelle
+
+import scala.util.parsing.combinator.RegexParsers
+
+
+object Scan
+{
+
+  /** Lexicon -- position tree **/
+
+  object Lexicon
+  {
+    private case class Tree(val branches: Map[Char, (String, Tree)])
+    private val empty_tree = Tree(Map())
+
+    private def make(tree: Tree, max: Int): Lexicon =
+      new Lexicon {
+        override val main_tree = tree
+        override val max_entry = max
+      }
+
+    val empty: Lexicon = new Lexicon
+    def apply(strs: String*): Lexicon = (empty /: strs) ((lex, str) => lex + str)
+  }
+
+  class Lexicon extends scala.collection.immutable.Set[String] with RegexParsers
+  {
+    /* representation */
+
+    import Lexicon.Tree
+    val main_tree: Tree = Lexicon.empty_tree
+    val max_entry = -1
+
+
+    /* auxiliary operations */
+
+    private def content(tree: Tree, result: List[String]): List[String] =
+      (result /: tree.branches.toList) ((res, entry) =>
+        entry match { case (_, (s, tr)) =>
+          if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
+
+    private def lookup(str: CharSequence): Option[(Boolean, Tree)] =
+    {
+      val len = str.length
+      def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] =
+      {
+        if (i < len) {
+          tree.branches.get(str.charAt(i)) match {
+            case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
+            case None => None
+          }
+        } else Some(tip, tree)
+      }
+      look(main_tree, false, 0)
+    }
+
+    def completions(str: CharSequence): List[String] =
+    {
+      (lookup(str) match {
+        case Some((true, tree)) => content(tree, List(str.toString))
+        case Some((false, tree)) => content(tree, Nil)
+        case None => Nil
+      }).sort((s1, s2) => s1.length < s2.length || s1.length == s2.length && s1 <= s2)
+    }
+
+
+    /* Set methods */
+
+    override def stringPrefix = "Lexicon"
+
+    override def isEmpty: Boolean = { max_entry < 0 }
+
+    def size: Int = content(main_tree, Nil).length
+    def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
+
+    def contains(str: String): Boolean =
+      lookup(str) match {
+        case Some((tip, _)) => tip
+        case _ => false
+      }
+
+    def +(str: String): Lexicon =
+    {
+      val len = str.length
+      def extend(tree: Tree, i: Int): Tree =
+      {
+        if (i < len) {
+          val c = str.charAt(i)
+          val end = (i + 1 == len)
+          tree.branches.get(c) match {
+            case Some((s, tr)) =>
+              Tree(tree.branches + (c -> (if (end) str else s, extend(tr, i + 1))))
+            case None =>
+              Tree(tree.branches + (c -> (if (end) str else "", extend(Lexicon.empty_tree, i + 1))))
+          }
+        } else tree
+      }
+      if (contains(str)) this
+      else Lexicon.make(extend(main_tree, 0), max_entry max str.length)
+    }
+
+    def empty[A]: Set[A] = error("Undefined")
+    def -(str: String): Lexicon = error("Undefined")
+
+
+    /* RegexParsers methods */
+
+    override val whiteSpace = "".r
+
+    def keyword: Parser[String] = new Parser[String] {
+      def apply(in: Input) =
+      {
+        val source = in.source
+        val offset = in.offset
+        val len = source.length - offset
+
+        def scan(tree: Tree, text: String, i: Int): String =
+        {
+          if (i < len) {
+            tree.branches.get(source.charAt(offset + i)) match {
+              case Some((s, tr)) => scan(tr, if (s.isEmpty) text else s, i + 1)
+              case None => text
+            }
+          } else text
+        }
+        val text = scan(main_tree, "", 0)
+        if (text.isEmpty) Failure("keyword expected", in)
+        else Success(text, in.drop(text.length))
+      }
+    }.named("keyword")
+
+  }
+}
+

--- a/src/Pure/General/symbol.scala	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Pure/General/symbol.scala	Wed Jun 17 10:08:06 2009 +0200
@@ -118,6 +118,18 @@
         yield read_decl(decl)
 
 
+    /* misc properties */
+
+    val names: Map[String, String] = {
+      val name = new Regex("""\\<([A-Za-z][A-Za-z0-9_']*)>""")
+      Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
+    }
+
+    val abbrevs: Map[String, String] = Map((
+      for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
+        yield (sym -> props("abbrev"))): _*)
+
+
     /* main recoder methods */
 
     private val (decoder, encoder) =

--- a/src/Pure/IsaMakefile	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Pure/IsaMakefile	Wed Jun 17 10:08:06 2009 +0200
@@ -115,9 +115,9 @@
 ## Scala material
 
 SCALA_FILES = General/event_bus.scala General/markup.scala		\
-  General/position.scala General/swing.scala General/symbol.scala	\
-  General/xml.scala General/yxml.scala Isar/isar.scala			\
-  Isar/isar_document.scala Isar/outer_keyword.scala			\
+  General/position.scala General/scan.scala General/swing.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/isabelle_process.scala			\
   System/isabelle_system.scala Thy/thy_header.scala			\
   Tools/isabelle_syntax.scala

--- a/src/Pure/Isar/code.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Pure/Isar/code.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -30,6 +30,7 @@
 
   (*code equations*)
   val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool
+  val mk_eqn_warning: theory -> (string -> bool) -> thm -> (thm * bool) option
   val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option
   val assert_eqn: theory -> thm * bool -> thm * bool
   val assert_eqns_const: theory -> string
@@ -72,6 +73,7 @@
   val get_datatype_of_constr: theory -> string -> string option
   val default_typscheme: theory -> string -> (string * sort) list * typ
   val these_eqns: theory -> string -> (thm * bool) list
+  val all_eqns: theory -> (thm * bool) list
   val get_case_scheme: theory -> string -> (int * (int * string list)) option
   val is_undefined: theory -> string -> bool
   val print_codesetup: theory -> unit
@@ -363,6 +365,7 @@
 exception BAD_THM of string;
 fun bad_thm msg = raise BAD_THM msg;
 fun error_thm f thm = f thm handle BAD_THM msg => error msg;
+fun warning_thm f thm = SOME (f thm) handle BAD_THM msg => (warning msg; NONE)
 fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
 
 fun is_linear thm =
@@ -445,6 +448,10 @@
 fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o
   apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy));
 
+fun mk_eqn_warning thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
+  o warning_thm (gen_assert_eqn thy is_constr_head (K true))
+  o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+
 fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm))
   o try_thm (gen_assert_eqn thy is_constr_head (K true))
   o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy);
@@ -861,6 +868,11 @@
 fun add_eqn thm thy =
   gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, true)) thy;
 
+fun add_warning_eqn thm thy =
+  case mk_eqn_warning thy (is_constr thy) thm
+   of SOME eqn => gen_add_eqn false eqn thy
+    | NONE => thy;
+
 fun add_default_eqn thm thy =
   case mk_eqn_liberal thy (is_constr thy) thm
    of SOME eqn => gen_add_eqn true eqn thy
@@ -938,7 +950,7 @@
         || Scan.succeed (mk_attribute add))
   in
     TypeInterpretation.init
-    #> add_del_attribute ("", (add_eqn, del_eqn))
+    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
     #> add_simple_attribute ("nbe", add_nbe_eqn)
   end));
 
@@ -947,6 +959,10 @@
   |> (map o apfst) (Thm.transfer thy)
   |> burrow_fst (common_typ_eqns thy);
 
+fun all_eqns thy =
+  Symtab.dest ((the_eqns o the_exec) thy)
+  |> maps (Lazy.force o snd o snd o fst o snd);
+
 fun default_typscheme thy c =
   let
     fun the_const_typscheme c = (curry (typscheme thy) c o snd o dest_Const

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -40,9 +40,16 @@
 
 val max_threads = ref 1;
 
+val tested_platform =
+  let val ml_platform = getenv "ML_PLATFORM"
+  in String.isSuffix "linux" ml_platform orelse String.isSuffix "darwin" ml_platform end;
+
 fun max_threads_value () =
-  let val m = ! max_threads
-  in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end;
+  let val m = ! max_threads in
+    if m > 0 then m
+    else if not tested_platform then 1
+    else Int.min (Int.max (Thread.numProcessors (), 1), 8)
+  end;
 
 fun enabled () = max_threads_value () > 1;
 

--- a/src/Pure/pure_setup.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Pure/pure_setup.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -4,15 +4,6 @@
 Pure theory and ML toplevel setup.
 *)
 
-(* ML toplevel use commands *)
-
-fun use name          = Toplevel.program (fn () => ThyInfo.use name);
-fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
-fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
-fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
-fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
-
-
 (* the Pure theories *)
 
 val theory = ThyInfo.get_theory;
@@ -49,6 +40,15 @@
 else ();
 
 
+(* ML toplevel use commands *)
+
+fun use name          = Toplevel.program (fn () => ThyInfo.use name);
+fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
+fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
+fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
+fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
+
+
 (* misc *)
 
 val cd = File.cd o Path.explode;

--- a/src/Tools/code/code_haskell.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Tools/code/code_haskell.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -106,11 +106,9 @@
               |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
-          in 
-            Pretty.block_enclose (
-              str "(let {",
-              concat [str "}", str "in", pr_term tyvars thm vars' NOBR body, str ")"]
-            ) ps
+          in brackify_block fxy (str "let {")
+            ps
+            (concat [str "}", str "in", pr_term tyvars thm vars' NOBR body])
           end
       | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
           let
@@ -118,11 +116,10 @@
               let
                 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
-          in
-            Pretty.block_enclose (
-              concat [str "(case", pr_term tyvars thm vars NOBR t, str "of", str "{"],
-              str "})"
-            ) (map pr clauses)
+          in brackify_block fxy
+            (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
+            (map pr clauses)
+            (str "}") 
           end
       | pr_case tyvars thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];

--- a/src/Tools/code/code_ml.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -151,7 +151,7 @@
                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
               end;
           in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
+            brackets (
               str "case"
               :: pr_term is_closure thm vars NOBR t
               :: pr "of" clause
@@ -441,8 +441,10 @@
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
-            fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
-          in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
+          in
+            brackify_block fxy (Pretty.chunks ps) []
+              (pr_term is_closure thm vars' NOBR body)
+          end
       | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun pr delim (pat, body) =
@@ -450,7 +452,7 @@
                 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
           in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
+            brackets (
               str "match"
               :: pr_term is_closure thm vars NOBR t
               :: pr "with" clause

--- a/src/Tools/code/code_printer.ML	Wed Jun 17 10:07:25 2009 +0200
+++ b/src/Tools/code/code_printer.ML	Wed Jun 17 10:08:06 2009 +0200
@@ -45,6 +45,7 @@
   val APP: fixity
   val brackify: fixity -> Pretty.T list -> Pretty.T
   val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
+  val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
 
   type itype = Code_Thingol.itype
   type iterm = Code_Thingol.iterm
@@ -175,6 +176,13 @@
 fun brackify_infix infx fxy_ctxt =
   gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
 
+fun brackify_block fxy_ctxt p1 ps p2 =
+  let val p = Pretty.block_enclose (p1, p2) ps
+  in if fixity BR fxy_ctxt
+    then Pretty.enclose "(" ")" [p]
+    else p
+  end;
+
 
 (* generic syntax *)