# HG changeset patch
# User wenzelm
# Date 1377809597 -7200
# Node ID 2ad60808295c461844eceb4c6f7b0f437769ceec
# Parent  050d0bc9afa5e02e8e9738f46d476879bba140d5# Parent  64c31de7f21c100da49c107b699b0b83f91277cd
merged

diff -r 050d0bc9afa5 -r 2ad60808295c NEWS
--- a/NEWS	Thu Aug 29 22:39:46 2013 +0200
+++ b/NEWS	Thu Aug 29 22:53:17 2013 +0200
@@ -96,6 +96,9 @@
 completed in backslash forms, e.g. \forall or \<forall> that both
 produce the Isabelle symbol \<forall> in its Unicode rendering.
 
+* Standard jEdit completion via C+b uses action isabelle.complete
+with fall-back on complete-word for non-Isabelle buffers.
+
 * Improved support for Linux look-and-feel "GTK+", see also "Utilities
 / Global Options / Appearance".
 
diff -r 050d0bc9afa5 -r 2ad60808295c src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 29 22:53:17 2013 +0200
@@ -55,11 +55,11 @@
 context topological_space
 begin
 
-definition "topological_basis B =
-  ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x)))"
+definition "topological_basis B \<longleftrightarrow>
+  (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
 
 lemma topological_basis:
-  "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
+  "topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
   unfolding topological_basis_def
   apply safe
      apply fastforce
@@ -198,7 +198,7 @@
   by (atomize_elim) simp
 
 lemma countable_dense_exists:
-  shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
+  "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
 proof -
   let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
   have "countable (?f ` B)" using countable_basis by simp
@@ -667,7 +667,7 @@
 lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
   by (simp add: closedin_subtopology closed_closedin Int_ac)
 
-lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)"
+lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)"
   by (metis closedin_closed)
 
 lemma closed_closedin_trans:
@@ -818,7 +818,7 @@
   apply (metis zero_le_dist order_trans dist_self)
   done
 
-lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
+lemma ball_empty[intro]: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp
 
 lemma euclidean_dist_l2:
   fixes x y :: "'a :: euclidean_space"
@@ -830,11 +830,11 @@
 
 lemma rational_boxes:
   fixes x :: "'a\<Colon>euclidean_space"
-  assumes "0 < e"
+  assumes "e > 0"
   shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e"
 proof -
   def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
-  then have e: "0 < e'"
+  then have e: "e' > 0"
     using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   proof
@@ -1087,7 +1087,7 @@
       by blast
     let ?m = "min (e/2) (dist x y) "
     from e2 y(2) have mp: "?m > 0"
-      by (simp add: dist_nz[THEN sym])
+      by (simp add: dist_nz[symmetric])
     from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
       by blast
     have th: "dist z y < e" using z y
@@ -1754,7 +1754,7 @@
 
 lemma Lim_at_zero:
   fixes a :: "'a::real_normed_vector"
-  fixes l :: "'b::topological_space"
+    and l :: "'b::topological_space"
   shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)"
   using LIM_offset_zero LIM_offset_zero_cancel ..
 
@@ -1880,7 +1880,8 @@
 
 lemma closure_sequential:
   fixes l :: "'a::first_countable_topology"
-  shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
+  shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)"
+  (is "?lhs = ?rhs")
 proof
   assume "?lhs"
   moreover
@@ -1917,7 +1918,7 @@
 
 lemma closed_approachable:
   fixes S :: "'a::metric_space set"
-  shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
+  shows "closed S \<Longrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
   by (metis closure_closed closure_approachable)
 
 lemma closure_contains_Inf:
@@ -2135,17 +2136,17 @@
   using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *)
 
 lemma seq_offset_neg:
-  "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
+  "(f ---> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) ---> l) sequentially"
   apply (rule topological_tendstoI)
   apply (drule (2) topological_tendstoD)
   apply (simp only: eventually_sequentially)
-  apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
+  apply (subgoal_tac "\<And>N k (n::nat). N + k <= n \<Longrightarrow> N <= n - k")
   apply metis
   apply arith
   done
 
 lemma seq_offset_rev:
-  "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
+  "((\<lambda>i. f(i + k)) ---> l) sequentially \<Longrightarrow> (f ---> l) sequentially"
   by (rule LIMSEQ_offset) (* FIXME: redundant *)
 
 lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially"
@@ -2184,7 +2185,7 @@
     unfolding open_contains_ball by auto
 qed
 
-lemma open_contains_cball_eq: "open S ==> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
+lemma open_contains_cball_eq: "open S \<Longrightarrow> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
   by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)
 
 lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
@@ -2196,7 +2197,8 @@
 
 lemma islimpt_ball:
   fixes x y :: "'a::{real_normed_vector,perfect_space}"
-  shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" (is "?lhs = ?rhs")
+  shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e"
+  (is "?lhs = ?rhs")
 proof
   assume "?lhs"
   {
@@ -2233,10 +2235,10 @@
         case False
         have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =
           norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
-          unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[THEN sym]
+          unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]
           by auto
         also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
-          using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
+          using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
           unfolding scaleR_minus_left scaleR_one
           by (auto simp add: norm_minus_commute)
         also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
@@ -2402,7 +2404,7 @@
         using d as(1)[unfolded subset_eq] by blast
       have "y - x \<noteq> 0" using `x \<noteq> y` by auto
       then have **:"d / (2 * norm (y - x)) > 0"
-        unfolding zero_less_norm_iff[THEN sym]
+        unfolding zero_less_norm_iff[symmetric]
         using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto
       have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
         norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
@@ -2427,7 +2429,7 @@
 
 lemma frontier_ball:
   fixes a :: "'a::real_normed_vector"
-  shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
+  shows "0 < e \<Longrightarrow> frontier(ball a e) = {x. dist a x = e}"
   apply (simp add: frontier_def closure_ball interior_open order_less_imp_le)
   apply (simp add: set_eq_iff)
   apply arith
@@ -2463,7 +2465,7 @@
 
 lemma cball_sing:
   fixes x :: "'a::metric_space"
-  shows "e = 0 ==> cball x e = {x}"
+  shows "e = 0 \<Longrightarrow> cball x e = {x}"
   by (auto simp add: set_eq_iff)
 
 
@@ -2501,10 +2503,10 @@
 lemma bounded_empty [simp]: "bounded {}"
   by (simp add: bounded_def)
 
-lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
+lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> bounded S"
   by (metis bounded_def subset_eq)
 
-lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)"
+lemma bounded_interior[intro]: "bounded S \<Longrightarrow> bounded(interior S)"
   by (metis bounded_subset interior_subset)
 
 lemma bounded_closure[intro]:
@@ -2583,7 +2585,7 @@
 lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
   by (metis Int_lower1 Int_lower2 bounded_subset)
 
-lemma bounded_diff[intro]: "bounded S ==> bounded (S - T)"
+lemma bounded_diff[intro]: "bounded S \<Longrightarrow> bounded (S - T)"
   by (metis Diff_subset bounded_subset)
 
 lemma not_bounded_UNIV[simp, intro]:
@@ -2599,8 +2601,9 @@
 qed
 
 lemma bounded_linear_image:
-  assumes "bounded S" "bounded_linear f"
-  shows "bounded(f ` S)"
+  assumes "bounded S"
+    and "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
@@ -2626,7 +2629,8 @@
 lemma bounded_scaling:
   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 (rule bounded_linear_image)
+  apply assumption
   apply (rule bounded_linear_scaleR_right)
   done
 
@@ -2654,7 +2658,7 @@
 
 lemma bounded_real:
   fixes S :: "real set"
-  shows "bounded S \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
+  shows "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. abs x \<le> a)"
   by (simp add: bounded_iff)
 
 lemma bounded_has_Sup:
@@ -2674,7 +2678,7 @@
 
 lemma Sup_insert:
   fixes S :: "real set"
-  shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
+  shows "bounded S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
   apply (subst cSup_insert_If)
   apply (rule bounded_has_Sup(1)[of S, rule_format])
   apply (auto simp: sup_max)
@@ -2682,7 +2686,7 @@
 
 lemma Sup_insert_finite:
   fixes S :: "real set"
-  shows "finite S \<Longrightarrow> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
+  shows "finite S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
   apply (rule Sup_insert)
   apply (rule finite_imp_bounded)
   apply simp
@@ -2707,7 +2711,7 @@
 
 lemma Inf_insert:
   fixes S :: "real set"
-  shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
+  shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
   apply (subst cInf_insert_if)
   apply (rule bounded_has_Inf(1)[of S, rule_format])
   apply (auto simp: inf_min)
@@ -2715,7 +2719,7 @@
 
 lemma Inf_insert_finite:
   fixes S :: "real set"
-  shows "finite S \<Longrightarrow> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
+  shows "finite S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
   apply (rule Inf_insert)
   apply (rule finite_imp_bounded)
   apply simp
@@ -2726,9 +2730,9 @@
 subsubsection {* Bolzano-Weierstrass property *}
 
 lemma heine_borel_imp_bolzano_weierstrass:
-  assumes "compact s" "infinite t"  "t \<subseteq> s"
+  assumes "compact s" and "infinite t" and "t \<subseteq> s"
   shows "\<exists>x \<in> s. x islimpt t"
-proof(rule ccontr)
+proof (rule ccontr)
   assume "\<not> (\<exists>x \<in> s. x islimpt t)"
   then obtain f where f:"\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)"
     unfolding islimpt_def
@@ -2981,7 +2985,8 @@
 text{* In particular, some common special cases. *}
 
 lemma compact_union [intro]:
-  assumes "compact s" "compact t"
+  assumes "compact s"
+    and "compact t"
   shows " compact (s \<union> t)"
 proof (rule compactI)
   fix f
@@ -3411,7 +3416,10 @@
   using assms unfolding seq_compact_def by fast
 
 lemma countably_compact_imp_acc_point:
-  assumes "countably_compact s" "countable t" "infinite t"  "t \<subseteq> s"
+  assumes "countably_compact s"
+    and "countable t"
+    and "infinite t"
+    and "t \<subseteq> s"
   shows "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)"
 proof (rule ccontr)
   def C \<equiv> "(\<lambda>F. interior (F \<union> (- t))) ` {F. finite F \<and> F \<subseteq> t }"
@@ -3445,7 +3453,8 @@
 
 lemma countable_acc_point_imp_seq_compact:
   fixes s :: "'a::first_countable_topology set"
-  assumes "\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
+  assumes "\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s \<longrightarrow>
+    (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
   shows "seq_compact s"
 proof -
   {
@@ -3487,7 +3496,8 @@
 
 lemma seq_compact_eq_acc_point:
   fixes s :: "'a :: first_countable_topology set"
-  shows "seq_compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s --> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)))"
+  shows "seq_compact s \<longleftrightarrow>
+    (\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s --> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)))"
   using
     countable_acc_point_imp_seq_compact[of s]
     countably_compact_imp_acc_point[of s]
@@ -3670,7 +3680,8 @@
 
 lemma compact_eq_bounded_closed:
   fixes s :: "'a::heine_borel set"
-  shows "compact s \<longleftrightarrow> bounded s \<and> closed s"  (is "?lhs = ?rhs")
+  shows "compact s \<longleftrightarrow> bounded s \<and> closed s"
+  (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then show ?rhs
@@ -3707,8 +3718,8 @@
 lemma compact_lemma:
   fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
   assumes "bounded (range f)"
-  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. subseq r \<and>
-        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
+    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
 proof safe
   fix d :: "'a set"
   assume d: "d \<subseteq> Basis"
@@ -4133,28 +4144,30 @@
 
 lemma compact_frontier_bounded[intro]:
   fixes s :: "'a::heine_borel set"
-  shows "bounded s ==> compact(frontier s)"
+  shows "bounded s \<Longrightarrow> compact(frontier s)"
   unfolding frontier_def
   using compact_eq_bounded_closed
   by blast
 
 lemma compact_frontier[intro]:
   fixes s :: "'a::heine_borel set"
-  shows "compact s ==> compact (frontier s)"
+  shows "compact s \<Longrightarrow> compact (frontier s)"
   using compact_eq_bounded_closed compact_frontier_bounded
   by blast
 
 lemma frontier_subset_compact:
   fixes s :: "'a::heine_borel set"
-  shows "compact s ==> frontier s \<subseteq> s"
+  shows "compact s \<Longrightarrow> frontier s \<subseteq> s"
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
 
 subsection {* Bounded closed nest property (proof does not use Heine-Borel) *}
 
 lemma bounded_closed_nest:
-  assumes "\<forall>n. closed(s n)" "\<forall>n. (s n \<noteq> {})"
-    "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)"  "bounded(s 0)"
+  assumes "\<forall>n. closed(s n)"
+    and "\<forall>n. (s n \<noteq> {})"
+    and "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)"
+    and "bounded(s 0)"
   shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s(n)"
 proof -
   from assms(2) obtain x where x:"\<forall>n::nat. x n \<in> s n"
@@ -4296,8 +4309,8 @@
 lemma uniformly_convergent_eq_cauchy:
   fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
   shows
-    "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow>
-      (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  --> dist (s m x) (s n x) < e)"
+    "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e) \<longleftrightarrow>
+      (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  \<longrightarrow> dist (s m x) (s n x) < e)"
   (is "?lhs = ?rhs")
 proof
   assume ?lhs
@@ -4328,7 +4341,7 @@
     apply auto
     done
   then obtain l where l: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l x) sequentially"
-    unfolding convergent_eq_cauchy[THEN sym]
+    unfolding convergent_eq_cauchy[symmetric]
     using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l) sequentially"]
     by auto
   {
@@ -4358,11 +4371,11 @@
 lemma uniformly_cauchy_imp_uniformly_convergent:
   fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
   assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
-          "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)"
-  shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e"
+    and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
+  shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
 proof -
   obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e"
-    using assms(1) unfolding uniformly_convergent_eq_cauchy[THEN sym] by auto
+    using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
   moreover
   {
     fix x
@@ -4383,7 +4396,7 @@
   "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
   unfolding continuous_within and Lim_within
   apply auto
-  unfolding dist_nz[THEN sym]
+  unfolding dist_nz[symmetric]
   apply (auto del: allE elim!:allE)
   apply(rule_tac x=d in exI)
   apply auto
@@ -4411,7 +4424,7 @@
       assume "y \<in> f ` (ball x d \<inter> s)"
       then have "y \<in> ball (f x) e"
         using d(2)
-        unfolding dist_nz[THEN sym]
+        unfolding dist_nz[symmetric]
         apply (auto simp add: dist_commute)
         apply (erule_tac x=xa in ballE)
         apply auto
@@ -4447,7 +4460,7 @@
     apply auto
     apply (erule_tac x=xa in allE)
     apply (auto simp add: dist_commute dist_nz)
-    unfolding dist_nz[THEN sym]
+    unfolding dist_nz[symmetric]
     apply auto
     done
 next
@@ -4534,7 +4547,7 @@
     proof eventually_elim
       case (elim n)
       then show ?case
-        using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
+        using d x(1) `f a \<in> T` unfolding dist_nz[symmetric] by auto
     qed
   }
   then show ?rhs
@@ -4548,15 +4561,16 @@
 
 lemma continuous_at_sequentially:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
-  shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
-                  --> ((f o x) ---> f a) sequentially)"
+  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] by simp
 
 lemma continuous_on_sequentially:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   shows "continuous_on s f \<longleftrightarrow>
     (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
-                    --> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")
+      --> ((f o x) ---> f(a)) sequentially)"
+  (is "?lhs = ?rhs")
 proof
   assume ?rhs
   then show ?lhs
@@ -4878,7 +4892,7 @@
 qed
 
 lemma continuous_closed_in_preimage:
-  assumes "continuous_on s f"  "closed t"
+  assumes "continuous_on s f" and "closed t"
   shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
 proof -
   have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> f ` s)"
@@ -4892,7 +4906,9 @@
 qed
 
 lemma continuous_open_preimage:
-  assumes "continuous_on s f" "open s" "open t"
+  assumes "continuous_on s f"
+    and "open s"
+    and "open t"
   shows "open {x \<in> s. f x \<in> t}"
 proof-
   obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
@@ -4902,7 +4918,9 @@
 qed
 
 lemma continuous_closed_preimage:
-  assumes "continuous_on s f" "closed s" "closed t"
+  assumes "continuous_on s f"
+    and "closed s"
+    and "closed t"
   shows "closed {x \<in> s. f x \<in> t}"
 proof-
   obtain T where "closed T" "{x \<in> s. f x \<in> t} = s \<inter> T"
@@ -4916,7 +4934,7 @@
   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}"
+  "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s \<Longrightarrow> 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: "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
@@ -4926,7 +4944,8 @@
   unfolding vimage_def by (rule continuous_closed_preimage_univ)
 
 lemma interior_image_subset:
-  assumes "\<forall>x. continuous (at x) f" "inj f"
+  assumes "\<forall>x. continuous (at x) f"
+    and "inj f"
   shows "interior (f ` s) \<subseteq> f ` (interior s)"
 proof
   fix x assume "x \<in> interior (f ` s)"
@@ -4947,12 +4966,12 @@
 
 lemma continuous_closed_in_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
-  shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
+  shows "continuous_on s f \<Longrightarrow> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
   using continuous_closed_in_preimage[of s f "{a}"] by auto
 
 lemma continuous_closed_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
-  shows "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
+  shows "continuous_on s f \<Longrightarrow> closed s \<Longrightarrow> closed {x \<in> s. f x = a}"
   using continuous_closed_preimage[of s f "{a}"] by auto
 
 lemma continuous_constant_on_closure:
@@ -4966,7 +4985,9 @@
     by auto
 
 lemma image_closure_subset:
-  assumes "continuous_on (closure s) f"  "closed t"  "(f ` s) \<subseteq> t"
+  assumes "continuous_on (closure s) f"
+    and "closed t"
+    and "(f ` s) \<subseteq> t"
   shows "f ` (closure s) \<subseteq> t"
 proof -
   have "s \<subseteq> {x \<in> closure s. f x \<in> t}"
@@ -4983,10 +5004,10 @@
   assumes "continuous_on (closure s) f"
     and "\<forall>y \<in> s. norm(f y) \<le> b"
     and "x \<in> (closure s)"
-  shows "norm(f x) \<le> b"
+  shows "norm (f x) \<le> b"
 proof -
   have *: "f ` s \<subseteq> cball 0 b"
-    using assms(2)[unfolded mem_cball_0[THEN sym]] by auto
+    using assms(2)[unfolded mem_cball_0[symmetric]] by auto
   show ?thesis
     using image_closure_subset[OF assms(1) closed_cball[of 0 b] *] assms(3)
     unfolding subset_eq
@@ -5002,7 +5023,7 @@
   assumes "continuous (at x within s) f"
     and "f x \<noteq> a"
   shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
-proof-
+proof -
   obtain U where "open U" and "f x \<in> U" and "a \<notin> U"
     using t1_space [OF `f x \<noteq> a`] by fast
   have "(f ---> f x) (at x within s)"
@@ -5036,7 +5057,10 @@
 
 lemma continuous_on_open_avoid:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
-  assumes "continuous_on s f"  "open s"  "x \<in> s"  "f x \<noteq> a"
+  assumes "continuous_on s f"
+    and "open s"
+    and "x \<in> s"
+    and "f x \<noteq> a"
   shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
   using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]
   using continuous_at_avoid[of x f a] assms(4)
@@ -5056,7 +5080,7 @@
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
         openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
-        (\<exists>x \<in> s. f x = a)  ==> (\<forall>x \<in> s. f x = a)"
+        (\<exists>x \<in> s. f x = a)  \<Longrightarrow> (\<forall>x \<in> s. f x = a)"
   using continuous_levelset_open_in_cases[of s f ]
   by meson
 
@@ -5075,7 +5099,8 @@
 
 lemma open_scaling[intro]:
   fixes s :: "'a::real_normed_vector set"
-  assumes "c \<noteq> 0"  "open s"
+  assumes "c \<noteq> 0"
+    and "open s"
   shows "open((\<lambda>x. c *\<^sub>R x) ` s)"
 proof -
   {
@@ -5085,7 +5110,7 @@
       and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
       by auto
     have "e * abs c > 0"
-      using assms(1)[unfolded zero_less_abs_iff[THEN sym]]
+      using assms(1)[unfolded zero_less_abs_iff[symmetric]]
       using mult_pos_pos[OF `e>0`]
       by auto
     moreover
@@ -5095,7 +5120,7 @@
       then have "norm ((1 / c) *\<^sub>R y - x) < e"
         unfolding dist_norm
         using norm_scaleR[of c "(1 / c) *\<^sub>R y - x", unfolded scaleR_right_diff_distrib, unfolded scaleR_scaleR] assms(1)
-          assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
+          assms(1)[unfolded zero_less_abs_iff[symmetric]] by (simp del:zero_less_abs_iff)
       then have "y \<in> op *\<^sub>R c ` s"
         using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "op *\<^sub>R c"]
         using e[THEN spec[where x="(1 / c) *\<^sub>R y"]]
@@ -5118,13 +5143,14 @@
 
 lemma open_negations:
   fixes s :: "'a::real_normed_vector set"
-  shows "open s ==> open ((\<lambda> x. -x) ` s)"
+  shows "open s \<Longrightarrow> open ((\<lambda> x. -x) ` s)"
   unfolding scaleR_minus1_left [symmetric]
   by (rule open_scaling, auto)
 
 lemma open_translation:
   fixes s :: "'a::real_normed_vector set"
-  assumes "open s"  shows "open((\<lambda>x. a + x) ` s)"
+  assumes "open s"
+  shows "open((\<lambda>x. a + x) ` s)"
 proof -
   {
     fix x
@@ -5164,7 +5190,7 @@
     unfolding subset_eq Ball_def mem_ball dist_norm
     apply auto
     apply (erule_tac x="a + xa" in allE)
-    unfolding ab_group_add_class.diff_diff_eq[THEN sym]
+    unfolding ab_group_add_class.diff_diff_eq[symmetric]
     apply auto
     done
   then show "x \<in> op + a ` interior s"
@@ -5217,11 +5243,11 @@
   done
 
 lemma linear_continuous_within:
-  "bounded_linear f ==> continuous (at x within s) f"
+  "bounded_linear f \<Longrightarrow> 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:
-  "bounded_linear f ==> continuous_on s f"
+  "bounded_linear f \<Longrightarrow> 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. *}
@@ -5293,12 +5319,17 @@
 qed
 
 lemma connected_continuous_image:
-  assumes "continuous_on s f"  "connected s"
+  assumes "continuous_on s f"
+    and "connected s"
   shows "connected(f ` s)"
 proof -
   {
     fix T
-    assume as: "T \<noteq> {}"  "T \<noteq> f ` s"  "openin (subtopology euclidean (f ` s)) T"  "closedin (subtopology euclidean (f ` s)) T"
+    assume as:
+      "T \<noteq> {}"
+      "T \<noteq> f ` s"
+      "openin (subtopology euclidean (f ` s)) T"
+      "closedin (subtopology euclidean (f ` s)) T"
     have "{x \<in> s. f x \<in> T} = {} \<or> {x \<in> s. f x \<in> T} = s"
       using assms(1)[unfolded continuous_on_open, THEN spec[where x=T]]
       using assms(1)[unfolded continuous_on_closed, THEN spec[where x=T]]
@@ -5313,7 +5344,8 @@
 text {* Continuity implies uniform continuity on a compact domain. *}
 
 lemma compact_uniformly_continuous:
-  assumes f: "continuous_on s f" and s: "compact s"
+  assumes f: "continuous_on s f"
+    and s: "compact s"
   shows "uniformly_continuous_on s f"
   unfolding uniformly_continuous_on_def
 proof (cases, safe)
@@ -5415,7 +5447,7 @@
   shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
   unfolding continuous_at
   unfolding Lim_at
-  unfolding dist_nz[THEN sym]
+  unfolding dist_nz[symmetric]
   unfolding dist_norm
   apply auto
   apply (erule_tac x=e in allE)
@@ -5454,7 +5486,8 @@
 
 lemma distance_attains_inf:
   fixes a :: "'a::heine_borel"
-  assumes "closed s"  "s \<noteq> {}"
+  assumes "closed s"
+    and "s \<noteq> {}"
   shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a x \<le> dist a y"
 proof -
   from assms(2) obtain b where "b \<in> s" by auto
@@ -5569,12 +5602,13 @@
 lemma compact_negations:
   fixes s :: "'a::real_normed_vector set"
   assumes "compact s"
-  shows "compact ((\<lambda>x. -x) ` s)"
+  shows "compact ((\<lambda>x. - x) ` s)"
   using compact_scaling [OF assms, of "- 1"] by auto
 
 lemma compact_sums:
   fixes s t :: "'a::real_normed_vector set"
-  assumes "compact s" and "compact t"
+  assumes "compact s"
+    and "compact t"
   shows "compact {x + y | x y. x \<in> s \<and> y \<in> t}"
 proof -
   have *: "{x + y | x y. x \<in> s \<and> y \<in> t} = (\<lambda>z. fst z + snd z) ` (s \<times> t)"
@@ -5591,7 +5625,9 @@
 
 lemma compact_differences:
   fixes s t :: "'a::real_normed_vector set"
-  assumes "compact s" "compact t"  shows "compact {x - y | x y. x \<in> s \<and> y \<in> t}"
+  assumes "compact s"
+    and "compact t"
+  shows "compact {x - y | x y. x \<in> s \<and> y \<in> t}"
 proof-
   have "{x - y | x y. x\<in>s \<and> y \<in> t} =  {x + y | x y. x \<in> s \<and> y \<in> (uminus ` t)}"
     apply auto
@@ -5630,7 +5666,8 @@
 
 lemma compact_sup_maxdistance:
   fixes s :: "'a::metric_space set"
-  assumes "compact s"  "s \<noteq> {}"
+  assumes "compact s"
+    and "s \<noteq> {}"
   shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
 proof -
   have "compact (s \<times> s)"
@@ -5688,17 +5725,19 @@
 lemma diameter_bounded:
   assumes "bounded s"
   shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"
-        "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. dist x y > d)"
+    and "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. dist x y > d)"
   using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms
   by auto
 
 lemma diameter_compact_attained:
-  assumes "compact s"  "s \<noteq> {}"
+  assumes "compact s"
+    and "s \<noteq> {}"
   shows "\<exists>x\<in>s. \<exists>y\<in>s. dist x y = diameter s"
 proof -
   have b: "bounded s" using assms(1)
     by (rule compact_imp_bounded)
-  then obtain x y where xys: "x\<in>s" "y\<in>s" and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
+  then obtain x y where xys: "x\<in>s" "y\<in>s"
+    and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
     using compact_sup_maxdistance[OF assms] by auto
   then have "diameter s \<le> dist x y"
     unfolding diameter_def
@@ -5752,7 +5791,7 @@
           using as(2)[unfolded LIMSEQ_def, THEN spec[where x="e * abs c"]] by auto
         then have "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
           unfolding dist_norm
-          unfolding scaleR_right_diff_distrib[THEN sym]
+          unfolding scaleR_right_diff_distrib[symmetric]
           using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto
       }
       then have "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially"
@@ -5795,7 +5834,9 @@
       unfolding o_def
       by auto
     then have "l - l' \<in> t"
-      using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda> n. snd (f (r n))"], THEN spec[where x="l - l'"]]
+      using assms(2)[unfolded closed_sequential_limits,
+        THEN spec[where x="\<lambda> n. snd (f (r n))"],
+        THEN spec[where x="l - l'"]]
       using f(3)
       by auto
     then have "l \<in> ?S"
@@ -5812,7 +5853,8 @@
 
 lemma closed_compact_sums:
   fixes s t :: "'a::real_normed_vector set"
-  assumes "closed s"  "compact t"
+  assumes "closed s"
+    and "compact t"
   shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}"
 proof -
   have "{x + y |x y. x \<in> t \<and> y \<in> s} = {x + y |x y. x \<in> s \<and> y \<in> t}"
@@ -5828,7 +5870,8 @@
 
 lemma compact_closed_differences:
   fixes s t :: "'a::real_normed_vector set"
-  assumes "compact s" and "closed t"
+  assumes "compact s"
+    and "closed t"
   shows "closed {x - y | x y. x \<in> s \<and> y \<in> t}"
 proof -
   have "{x + y |x y. x \<in> s \<and> y \<in> uminus ` t} =  {x - y |x y. x \<in> s \<and> y \<in> t}"
@@ -5844,7 +5887,8 @@
 
 lemma closed_compact_differences:
   fixes s t :: "'a::real_normed_vector set"
-  assumes "closed s" "compact t"
+  assumes "closed s"
+    and "compact t"
   shows "closed {x - y | x y. x \<in> s \<and> y \<in> t}"
 proof -
   have "{x + y |x y. x \<in> s \<and> y \<in> uminus ` t} = {x - y |x y. x \<in> s \<and> y \<in> t}"
@@ -5917,7 +5961,8 @@
 
 lemma separate_point_closed:
   fixes s :: "'a::heine_borel set"
-  assumes "closed s" and "a \<notin> s"
+  assumes "closed s"
+    and "a \<notin> s"
   shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
 proof (cases "s = {}")
   case True
@@ -6049,7 +6094,8 @@
 
 lemma interval_sing:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "{a .. a} = {a}" and "{a<..<a} = {}"
+  shows "{a .. a} = {a}"
+    and "{a<..<a} = {}"
   unfolding set_eq_iff mem_interval eq_iff [symmetric]
   by (auto intro: euclidean_eqI simp: ex_in_conv)
 
@@ -6173,7 +6219,8 @@
 
 lemma inter_interval:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "{a .. b} \<inter> {c .. d} =  {(\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)}"
+  shows "{a .. b} \<inter> {c .. d} =
+    {(\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)}"
   unfolding set_eq_iff and Int_iff and mem_interval
   by auto
 
@@ -6225,7 +6272,8 @@
   fixes a b :: "'a::ordered_euclidean_space"
   shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
 proof(rule subset_antisym)
-  show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
+  show "?R \<subseteq> ?L"
+    using interval_open_subset_closed open_interval
     by (rule interior_maximal)
   {
     fix x
@@ -6296,7 +6344,7 @@
 
 lemma not_interval_univ:
   fixes a :: "'a::ordered_euclidean_space"
-  shows "({a .. b} \<noteq> UNIV) \<and> ({a<..<b} \<noteq> UNIV)"
+  shows "{a .. b} \<noteq> UNIV \<and> {a<..<b} \<noteq> UNIV"
   using bounded_interval[of a b] by auto
 
 lemma compact_interval:
@@ -6462,12 +6510,13 @@
 
 lemma bounded_subset_open_interval:
   fixes s :: "('a::ordered_euclidean_space) set"
-  shows "bounded s ==> (\<exists>a b. s \<subseteq> {a<..<b})"
+  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> {a<..<b})"
   by (auto dest!: bounded_subset_open_interval_symmetric)
 
 lemma bounded_subset_closed_interval_symmetric:
   fixes s :: "('a::ordered_euclidean_space) set"
-  assumes "bounded s" shows "\<exists>a. s \<subseteq> {-a .. a}"
+  assumes "bounded s"
+  shows "\<exists>a. s \<subseteq> {-a .. a}"
 proof -
   obtain a where "s \<subseteq> {- a<..<a}"
     using bounded_subset_open_interval_symmetric[OF assms] by auto
@@ -6477,7 +6526,7 @@
 
 lemma bounded_subset_closed_interval:
   fixes s :: "('a::ordered_euclidean_space) set"
-  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> {a .. b})"
+  shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> {a .. b}"
   using bounded_subset_closed_interval_symmetric[of s] by auto
 
 lemma frontier_closed_interval:
@@ -6503,7 +6552,7 @@
   fixes a :: "'a::ordered_euclidean_space"
   assumes "{c<..<d} \<noteq> {}"
   shows "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> {a<..<b} \<inter> {c<..<d} = {}"
-  unfolding closure_open_interval[OF assms, THEN sym]
+  unfolding closure_open_interval[OF assms, symmetric]
   unfolding open_inter_closure_eq_empty[OF open_interval] ..
 
 
@@ -6815,7 +6864,11 @@
 text{* Some more convenient intermediate-value theorem formulations. *}
 
 lemma connected_ivt_hyperplane:
-  assumes "connected s" "x \<in> s" "y \<in> s" "inner a x \<le> b" "b \<le> inner a y"
+  assumes "connected s"
+    and "x \<in> s"
+    and "y \<in> s"
+    and "inner a x \<le> b"
+    and "b \<le> inner a y"
   shows "\<exists>z \<in> s. inner a z = b"
 proof (rule ccontr)
   assume as:"\<not> (\<exists>z\<in>s. inner a z = b)"
@@ -6823,9 +6876,12 @@
   let ?B = "{x. inner a x > b}"
   have "open ?A" "open ?B"
     using open_halfspace_lt and open_halfspace_gt by auto
-  moreover have "?A \<inter> ?B = {}" by auto
-  moreover have "s \<subseteq> ?A \<union> ?B" using as by auto
-  ultimately show False
+  moreover
+  have "?A \<inter> ?B = {}" by auto
+  moreover
+  have "s \<subseteq> ?A \<union> ?B" using as by auto
+  ultimately
+  show False
     using assms(1)[unfolded connected_def not_ex,
       THEN spec[where x="?A"], THEN spec[where x="?B"]]
     using assms(2-5)
@@ -6951,7 +7007,7 @@
     then obtain x where x:"f x = y" "x\<in>s"
       using assms(3) by auto
     then have "g (f x) = x" using g by auto
-    then have "f (g y) = y" unfolding x(1)[THEN sym] by auto
+    then have "f (g y) = y" unfolding x(1)[symmetric] by auto
   }
   then have g':"\<forall>x\<in>t. f (g x) = x" by auto
   moreover
@@ -6971,7 +7027,7 @@
       then have "x \<in> s"
         unfolding g_def
         using someI2[of "\<lambda>b. b\<in>s \<and> f b = y" x' "\<lambda>x. x\<in>s"]
-        unfolding y(2)[THEN sym] and g_def
+        unfolding y(2)[symmetric] and g_def
         by auto
     }
     ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" ..
@@ -7069,9 +7125,11 @@
 proof -
   interpret f: bounded_linear f by fact
   {
-    fix d::real assume "d>0"
+    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]
+      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
@@ -7082,7 +7140,7 @@
         using normf[THEN bspec[where x="x n - x N"]]
         by auto
       also have "norm (f (x n - x N)) < e * d"
-        using `N \<le> n` N unfolding f.diff[THEN sym] by auto
+        using `N \<le> n` N unfolding f.diff[symmetric] by auto
       finally have "norm (x n - x N) < d" using `e>0` by simp
     }
     then have "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto
@@ -7091,13 +7149,13 @@
 qed
 
 lemma complete_isometric_image:
-  fixes f :: "'a::euclidean_space => 'b::euclidean_space"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   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)"
+  shows "complete (f ` s)"
 proof -
   {
     fix g
@@ -7156,7 +7214,7 @@
   then obtain b where "b\<in>s"
     and ba: "norm b = norm a"
     and b: "\<forall>x\<in>{x \<in> s. norm x = norm a}. norm (f b) \<le> norm (f x)"
-    unfolding *[THEN sym] unfolding image_iff by auto
+    unfolding *[symmetric] unfolding image_iff by auto
 
   let ?e = "norm (f b) / norm b"
   have "norm b > 0" using ba and a and norm_ge_zero by auto
@@ -7179,7 +7237,7 @@
       case False
       then have *: "0 < norm a / norm x"
         using `a\<noteq>0`
-        unfolding zero_less_norm_iff[THEN sym]
+        unfolding zero_less_norm_iff[symmetric]
         by (simp only: divide_pos_pos)
       have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s"
         using s[unfolded subspace_def] by auto
@@ -7203,7 +7261,7 @@
     using injective_imp_isometric[OF assms(4,1,2,3)] by auto
   show ?thesis
     using complete_isometric_image[OF `e>0` assms(1,2) e] and assms(4)
-    unfolding complete_eq_closed[THEN sym] by auto
+    unfolding complete_eq_closed[symmetric] by auto
 qed
 
 
@@ -7299,7 +7357,7 @@
 qed
 
 lemma closed_subspace:
-  fixes s::"('a::euclidean_space) set"
+  fixes s :: "'a::euclidean_space set"
   assumes "subspace s"
   shows "closed s"
 proof -
@@ -7349,36 +7407,37 @@
 subsection {* Affine transformations of intervals *}
 
 lemma real_affinity_le:
- "0 < (m::'a::linordered_field) ==> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
+ "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_le_affinity:
- "0 < (m::'a::linordered_field) ==> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
+ "0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_affinity_lt:
- "0 < (m::'a::linordered_field) ==> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
+ "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_lt_affinity:
- "0 < (m::'a::linordered_field) ==> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
+ "0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_affinity_eq:
- "(m::'a::linordered_field) \<noteq> 0 ==> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
+ "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma real_eq_affinity:
- "(m::'a::linordered_field) \<noteq> 0 ==> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
+ "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
   by (simp add: field_simps inverse_eq_divide)
 
 lemma image_affinity_interval: fixes m::real
   fixes a b c :: "'a::ordered_euclidean_space"
   shows "(\<lambda>x. m *\<^sub>R x + c) ` {a .. b} =
-            (if {a .. b} = {} then {}
-            else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
-            else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
+    (if {a .. b} = {} then {}
+     else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
+     else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
 proof (cases "m = 0")
+  case True
   {
     fix x
     assume "x \<le> c" "c \<le> x"
@@ -7389,9 +7448,9 @@
       apply (auto intro: order_antisym)
       done
   }
-  moreover case True
-  moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}" unfolding True by(auto simp add: eucl_le[where 'a='a])
-  ultimately show ?thesis by auto
+  moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}"
+    unfolding True by (auto simp add: eucl_le[where 'a='a])
+  ultimately show ?thesis using True by auto
 next
   case False
   {
@@ -7441,8 +7500,8 @@
   assumes s: "complete s" "s \<noteq> {}"
     and c: "0 \<le> c" "c < 1"
     and f: "(f ` s) \<subseteq> s"
-    and lipschitz:"\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
-  shows "\<exists>! x\<in>s. (f x = x)"
+    and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
+  shows "\<exists>!x\<in>s. f x = x"
 proof -
   have "1 - c > 0" using c by auto
 
diff -r 050d0bc9afa5 -r 2ad60808295c src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/Pure/General/time.scala	Thu Aug 29 22:53:17 2013 +0200
@@ -30,6 +30,7 @@
   def min(t: Time): Time = if (ms < t.ms) this else t
   def max(t: Time): Time = if (ms > t.ms) this else t
 
+  def is_zero: Boolean = ms == 0
   def is_relevant: Boolean = ms >= 1
 
   override def hashCode: Int = ms.hashCode
diff -r 050d0bc9afa5 -r 2ad60808295c src/Pure/Isar/completion.scala
--- a/src/Pure/Isar/completion.scala	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/Pure/Isar/completion.scala	Thu Aug 29 22:53:17 2013 +0200
@@ -13,7 +13,11 @@
 {
   /* items */
 
-  sealed case class Item(original: String, replacement: String, description: String)
+  sealed case class Item(
+    original: String,
+    replacement: String,
+    description: String,
+    immediate: Boolean)
   { override def toString: String = description }
 
 
@@ -105,9 +109,12 @@
       }
     raw_result match {
       case Some((word, cs)) =>
-        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
+        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs)
         if (ds.isEmpty) None
-        else Some((word, ds.map(s => Completion.Item(word, s, s))))
+        else {
+          val immediate = !Completion.is_word(word)
+          Some((word, ds.map(s => Completion.Item(word, s, s, immediate))))
+        }
       case None => None
     }
   }
diff -r 050d0bc9afa5 -r 2ad60808295c src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Aug 29 22:53:17 2013 +0200
@@ -33,12 +33,18 @@
 public option jedit_timing_threshold : real = 0.1
   -- "default threshold for timing display"
 
+
+section "Completion"
+
 public option jedit_completion : bool = true
   -- "enable completion popup"
 
 public option jedit_completion_delay : real = 0.0
   -- "delay for completion popup (seconds)"
 
+public option jedit_completion_immediate : bool = false
+  -- "insert unique completion immediately into buffer (if delay = 0)"
+
 
 section "Rendering of Document Content"
 
diff -r 050d0bc9afa5 -r 2ad60808295c src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Thu Aug 29 22:53:17 2013 +0200
@@ -117,6 +117,11 @@
 	    isabelle.jedit.Isabelle.decrease_font_size(view);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.complete">
+	  <CODE>
+	    isabelle.jedit.Isabelle.complete(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.control-sub">
 	  <CODE>
 	    isabelle.jedit.Isabelle.control_sub(textArea);
diff -r 050d0bc9afa5 -r 2ad60808295c src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 22:53:17 2013 +0200
@@ -9,14 +9,15 @@
 
 import isabelle._
 
-import java.awt.{Font, Point, BorderLayout, Dimension}
-import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
+import java.awt.{Color, Font, Point, BorderLayout, Dimension}
+import java.awt.event.{InputEvent, KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
 import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
+import javax.swing.border.LineBorder
 
 import scala.swing.{ListView, ScrollPane}
 import scala.swing.event.MouseClicked
 
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{View, Debug}
 import org.gjt.sp.jedit.textarea.JEditTextArea
 
 
@@ -66,26 +67,10 @@
 
   class Text_Area private(text_area: JEditTextArea)
   {
-    /* popup state */
-
     private var completion_popup: Option[Completion_Popup] = None
 
-    def dismissed(): Boolean =
-    {
-      Swing_Thread.require()
 
-      completion_popup match {
-        case Some(completion) =>
-          completion.hide_popup()
-          completion_popup = None
-          true
-        case None =>
-          false
-      }
-    }
-
-
-    /* insert selected item */
+    /* completion action */
 
     private def insert(item: Completion.Item)
     {
@@ -106,8 +91,56 @@
       }
     }
 
+    def action(immediate: Boolean)
+    {
+      val view = text_area.getView
+      val layered = view.getLayeredPane
+      val buffer = text_area.getBuffer
+      val painter = text_area.getPainter
 
-    /* input of key events */
+      if (buffer.isEditable) {
+        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
+          case Some(syntax) =>
+            val caret = text_area.getCaretPosition
+            val line = buffer.getLineOfOffset(caret)
+            val start = buffer.getLineStartOffset(line)
+            val text = buffer.getSegment(start, caret - start)
+
+            syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
+              case Some((_, List(item))) if item.immediate && immediate =>
+                insert(item)
+
+              case Some((original, items)) =>
+                val font =
+                  painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+
+                val loc1 = text_area.offsetToXY(caret - original.length)
+                if (loc1 != null) {
+                  val loc2 =
+                    SwingUtilities.convertPoint(painter,
+                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
+
+                  val completion =
+                    new Completion_Popup(layered, loc2, font, items) {
+                      override def complete(item: Completion.Item) { insert(item) }
+                      override def propagate(evt: KeyEvent) {
+                        JEdit_Lib.propagate_key(view, evt)
+                        input(evt)
+                      }
+                      override def refocus() { text_area.requestFocus }
+                    }
+                  completion_popup = Some(completion)
+                  completion.show_popup()
+                }
+              case None =>
+            }
+          case None =>
+        }
+      }
+    }
+
+
+    /* input key events */
 
     def input(evt: KeyEvent)
     {
@@ -116,60 +149,46 @@
       if (PIDE.options.bool("jedit_completion")) {
         if (!evt.isConsumed) {
           dismissed()
-          input_delay.invoke()
+
+          val mod = evt.getModifiers
+          val special =
+            evt.getKeyChar == '\b' ||
+            // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
+            (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
+            (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
+              !Debug.ALT_KEY_PRESSED_DISABLED ||
+            (mod & InputEvent.META_MASK) != 0
+
+          if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
+            input_delay.revoke()
+            action(PIDE.options.bool("jedit_completion_immediate"))
+          }
+          else input_delay.invoke()
         }
       }
-      else {
-        dismissed()
-        input_delay.revoke()
-      }
     }
 
     private val input_delay =
-      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay"))
-      {
-        val view = text_area.getView
-        val layered = view.getLayeredPane
-        val buffer = text_area.getBuffer
-        val painter = text_area.getPainter
+      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
+        action(false)
+      }
 
-        if (buffer.isEditable) {
-          Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
-            case Some(syntax) =>
-              val caret = text_area.getCaretPosition
-              val line = buffer.getLineOfOffset(caret)
-              val start = buffer.getLineStartOffset(line)
-              val text = buffer.getSegment(start, caret - start)
 
-              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
-                case Some((original, items)) =>
-                  val font =
-                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+    /* dismiss popup */
 
-                  val loc1 = text_area.offsetToXY(caret - original.length)
-                  if (loc1 != null) {
-                    val loc2 =
-                      SwingUtilities.convertPoint(painter,
-                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
+    def dismissed(): Boolean =
+    {
+      Swing_Thread.require()
 
-                    val completion =
-                      new Completion_Popup(layered, loc2, font, items) {
-                        override def complete(item: Completion.Item) { insert(item) }
-                        override def propagate(evt: KeyEvent) {
-                          JEdit_Lib.propagate_key(view, evt)
-                          input(evt)
-                        }
-                        override def refocus() { text_area.requestFocus }
-                      }
-                    completion_popup = Some(completion)
-                    completion.show_popup()
-                  }
-                case None =>
-              }
-            case None =>
-          }
-        }
+      completion_popup match {
+        case Some(completion) =>
+          completion.hide_popup()
+          completion_popup = None
+          true
+        case None =>
+          false
       }
+    }
 
 
     /* activation */
@@ -289,7 +308,7 @@
   /* main content */
 
   override def getFocusTraversalKeysEnabled = false
-
+  completion.setBorder(new LineBorder(Color.BLACK))
   completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
 
 
diff -r 050d0bc9afa5 -r 2ad60808295c src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 22:53:17 2013 +0200
@@ -11,7 +11,7 @@
 
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
 
 
 object Isabelle
@@ -163,6 +163,17 @@
   }
 
 
+  /* completion */
+
+  def complete(view: View)
+  {
+    Completion_Popup.Text_Area(view.getTextArea) match {
+      case Some(text_area_completion) => text_area_completion.action(true)
+      case None => CompleteWord.completeWord(view)
+    }
+  }
+
+
   /* control styles */
 
   def control_sub(text_area: JEditTextArea)
diff -r 050d0bc9afa5 -r 2ad60808295c src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Thu Aug 29 22:53:17 2013 +0200
@@ -190,6 +190,8 @@
 isabelle-sledgehammer.dock-position=bottom
 isabelle-symbols.dock-position=bottom
 isabelle-theories.dock-position=right
+isabelle.complete.label=Complete text
+isabelle.complete.shortcut=C+b
 isabelle.control-bold.label=Control bold
 isabelle.control-bold.shortcut=C+e RIGHT
 isabelle.control-reset.label=Control reset