# HG changeset patch
# User eberlm
# Date 1446546021 -3600
# Node ID 933eb9e6a1cc19ea1ad17c4f07a716b3a6d8f1ef
# Parent  980dd46a03fb538ff9d0846fed3e0ac2e5a9498d# Parent  078c9fd2e052d820425a72942771b804474996ac
Merged

diff -r 980dd46a03fb -r 933eb9e6a1cc Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Nov 02 16:17:09 2015 +0100
+++ b/Admin/components/components.sha1	Tue Nov 03 11:20:21 2015 +0100
@@ -2,6 +2,7 @@
 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
 a5e02b5e990da4275dc5d4480c3b72fc73160c28  cvc4-1.5pre-1.tar.gz
 4d9658fd2688ae8ac78da8fdfcbf85960f871b71  cvc4-1.5pre-2.tar.gz
+b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9  cvc4-1.5pre-3.tar.gz
 03aec2ec5757301c9df149f115d1f4f1d2cafd9e  cvc4-1.5pre.tar.gz
 842d9526f37b928cf9e22f141884365129990d63  cygwin-20130110.tar.gz
 cb3b0706d208f104b800267697204f6d82f7b48a  cygwin-20130114.tar.gz
diff -r 980dd46a03fb -r 933eb9e6a1cc Admin/components/main
--- a/Admin/components/main	Mon Nov 02 16:17:09 2015 +0100
+++ b/Admin/components/main	Tue Nov 03 11:20:21 2015 +0100
@@ -1,6 +1,6 @@
 #main components for everyday use, without big impact on overall build time
 csdp-6.x
-cvc4-1.5pre-2
+cvc4-1.5pre-3
 e-1.8
 exec_process-1.0.3
 Haskabelle-2015
diff -r 980dd46a03fb -r 933eb9e6a1cc NEWS
--- a/NEWS	Mon Nov 02 16:17:09 2015 +0100
+++ b/NEWS	Tue Nov 03 11:20:21 2015 +0100
@@ -79,6 +79,9 @@
 standard Isabelle fonts provide glyphs to render important control
 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
 
+* System option "document_symbols" determines completion of Isabelle
+symbols within document source.
+
 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
 text. Command-line tool "isabelle update_cartouches -t" helps to update
@@ -397,6 +400,9 @@
   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
     structure on the raw type to an abstract type defined using typedef.
   - Always generate "case_transfer" theorem.
+  - Allow discriminators and selectors with the same name as the type
+    being defined.
+  - Avoid various internal name clashes (e.g., 'datatype f = f').
 
 * Transfer:
   - new methods for interactive debugging of 'transfer' and
diff -r 980dd46a03fb -r 933eb9e6a1cc etc/options
--- a/etc/options	Mon Nov 02 16:17:09 2015 +0100
+++ b/etc/options	Tue Nov 03 11:20:21 2015 +0100
@@ -164,3 +164,5 @@
 public option completion_limit : int = 40
   -- "limit for completion within the formal context"
 
+public option document_symbols : bool = false
+  -- "completion of Isabelle symbols within document source"
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/BNF_Fixpoint_Base.thy
--- a/src/HOL/BNF_Fixpoint_Base.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -14,9 +14,6 @@
 imports BNF_Composition Basic_BNFs
 begin
 
-lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
-  by standard simp_all
-
 lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
   by standard simp_all
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Data_Structures/AList_Upd_Del.thy
--- a/src/HOL/Data_Structures/AList_Upd_Del.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -14,39 +14,39 @@
 hide_const (open) map_of
 
 fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where
-"map_of [] = (\<lambda>a. None)" |
-"map_of ((x,y)#ps) = (\<lambda>a. if x=a then Some y else map_of ps a)"
+"map_of [] = (\<lambda>x. None)" |
+"map_of ((a,b)#ps) = (\<lambda>x. if x=a then Some b else map_of ps x)"
 
 text \<open>Updating an association list:\<close>
 
 fun upd_list :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) list \<Rightarrow> ('a*'b) list" where
-"upd_list a b [] = [(a,b)]" |
-"upd_list a b ((x,y)#ps) =
-  (if a < x then (a,b)#(x,y)#ps else
-  if a=x then (a,b)#ps else (x,y) # upd_list a b ps)"
+"upd_list x y [] = [(x,y)]" |
+"upd_list x y ((a,b)#ps) =
+  (if x < a then (x,y)#(a,b)#ps else
+  if x = a then (x,y)#ps else (a,b) # upd_list x y ps)"
 
 fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where
-"del_list a [] = []" |
-"del_list a ((x,y)#ps) = (if a=x then ps else (x,y) # del_list a ps)"
+"del_list x [] = []" |
+"del_list x ((a,b)#ps) = (if x = a then ps else (a,b) # del_list x ps)"
 
 
 subsection \<open>Lemmas for @{const map_of}\<close>
 
-lemma map_of_ins_list: "map_of (upd_list a b ps) = (map_of ps)(a := Some b)"
+lemma map_of_ins_list: "map_of (upd_list x y ps) = (map_of ps)(x := Some y)"
 by(induction ps) auto
 
-lemma map_of_append: "map_of (ps @ qs) a =
-  (case map_of ps a of None \<Rightarrow> map_of qs a | Some b \<Rightarrow> Some b)"
+lemma map_of_append: "map_of (ps @ qs) x =
+  (case map_of ps x of None \<Rightarrow> map_of qs x | Some y \<Rightarrow> Some y)"
 by(induction ps)(auto)
 
-lemma map_of_None: "sorted (a # map fst ps) \<Longrightarrow> map_of ps a = None"
+lemma map_of_None: "sorted (x # map fst ps) \<Longrightarrow> map_of ps x = None"
 by (induction ps) (auto simp: sorted_lems sorted_Cons_iff)
 
-lemma map_of_None2: "sorted (map fst ps @ [a]) \<Longrightarrow> map_of ps a = None"
+lemma map_of_None2: "sorted (map fst ps @ [x]) \<Longrightarrow> map_of ps x = None"
 by (induction ps) (auto simp: sorted_lems)
 
 lemma map_of_del_list: "sorted1 ps \<Longrightarrow>
-  map_of(del_list a ps) = (map_of ps)(a := None)"
+  map_of(del_list x ps) = (map_of ps)(x := None)"
 by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff)
 
 lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow>
@@ -63,19 +63,19 @@
 
 subsection \<open>Lemmas for @{const upd_list}\<close>
 
-lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list a b ps)"
-apply(induction ps) 
+lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list x y ps)"
+apply(induction ps)
  apply simp
 apply(case_tac ps)
  apply auto
 done
 
-lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [x]); a < x \<rbrakk> \<Longrightarrow>
-  upd_list a b (ps @ (x,y) # qs) =  upd_list a b ps @ (x,y) # qs"
+lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [a]); x < a \<rbrakk> \<Longrightarrow>
+  upd_list x y (ps @ (a,b) # qs) =  upd_list x y ps @ (a,b) # qs"
 by(induction ps) (auto simp: sorted_lems)
 
-lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [x]); x \<le> a \<rbrakk> \<Longrightarrow>
-  upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)"
+lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [a]); a \<le> x \<rbrakk> \<Longrightarrow>
+  upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)"
 by(induction ps) (auto simp: sorted_lems)
 
 lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2
@@ -110,28 +110,28 @@
 lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs"
 by (induct xs) auto
 
-lemma del_list_sorted1: "sorted1 (xs @ [(x,y)]) \<Longrightarrow> x \<le> a \<Longrightarrow>
-  del_list a (xs @ (x,y) # ys) = xs @ del_list a ((x,y) # ys)"
+lemma del_list_sorted1: "sorted1 (xs @ [(a,b)]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+  del_list x (xs @ (a,b) # ys) = xs @ del_list x ((a,b) # ys)"
 by (induction xs) (auto simp: sorted_mid_iff2)
 
-lemma del_list_sorted2: "sorted1 (xs @ (x,y) # ys) \<Longrightarrow> a < x \<Longrightarrow>
-  del_list a (xs @ (x,y) # ys) = del_list a xs @ (x,y) # ys"
+lemma del_list_sorted2: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> x < a \<Longrightarrow>
+  del_list x (xs @ (a,b) # ys) = del_list x xs @ (a,b) # ys"
 by (induction xs) (fastforce simp: sorted_Cons_iff intro!: del_list_idem)+
 
 lemma del_list_sorted3:
-  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs) \<Longrightarrow> a < y \<Longrightarrow>
-  del_list a (xs @ (x,x') # ys @ (y,y') # zs) = del_list a (xs @ (x,x') # ys) @ (y,y') # zs"
+  "sorted1 (xs @ (a,a') # ys @ (b,b') # zs) \<Longrightarrow> x < b \<Longrightarrow>
+  del_list x (xs @ (a,a') # ys @ (b,b') # zs) = del_list x (xs @ (a,a') # ys) @ (b,b') # zs"
 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2 ball_Un)
 
 lemma del_list_sorted4:
-  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) \<Longrightarrow> a < z \<Longrightarrow>
-  del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) = del_list a (xs @ (x,x') # ys @ (y,y') # zs) @ (z,z') # us"
+  "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) \<Longrightarrow> x < c \<Longrightarrow>
+  del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) = del_list x (xs @ (a,a') # ys @ (b,b') # zs) @ (c,c') # us"
 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
 
 lemma del_list_sorted5:
-  "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) \<Longrightarrow> a < u \<Longrightarrow>
-   del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) =
-   del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) @ (u,u') # vs" 
+  "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) \<Longrightarrow> x < d \<Longrightarrow>
+   del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) =
+   del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) @ (d,d') # vs" 
 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
 
 lemmas del_list_sorted =
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -52,8 +52,8 @@
 
 fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "ins_list x [] = [x]" |
-"ins_list x (y#zs) =
-  (if x < y then x#y#zs else if x=y then x#zs else y # ins_list x zs)"
+"ins_list x (a#xs) =
+  (if x < a then x#a#xs else if x=a then a#xs else a # ins_list x xs)"
 
 lemma set_ins_list[simp]: "elems (ins_list x xs) = insert x (elems xs)"
 by(induction xs) auto
@@ -66,12 +66,12 @@
 lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
 by(induction xs rule: sorted.induct) auto
 
-lemma ins_list_sorted1: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow>
-  ins_list x (xs @ y # ys) = xs @ ins_list x (y#ys)"
+lemma ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+  ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)"
 by(induction xs) (auto simp: sorted_lems)
 
-lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow>
-  ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)"
+lemma ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow>
+  ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)"
 by(induction xs) (auto simp: sorted_lems)
 
 lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
@@ -80,8 +80,8 @@
 subsection \<open>Delete one occurrence of an element from a list:\<close>
 
 fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"del_list a [] = []" |
-"del_list a (x#xs) = (if a=x then xs else x # del_list a xs)"
+"del_list x [] = []" |
+"del_list x (a#xs) = (if x=a then xs else a # del_list x xs)"
 
 lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs"
 by (induct xs) simp_all
@@ -99,28 +99,28 @@
 apply auto
 by (meson order.strict_trans sorted_Cons_iff)
 
-lemma del_list_sorted1: "sorted (xs @ [x]) \<Longrightarrow> x \<le> y \<Longrightarrow>
-  del_list y (xs @ x # ys) = xs @ del_list y (x # ys)"
+lemma del_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow>
+  del_list x (xs @ a # ys) = xs @ del_list x (a # ys)"
 by (induction xs) (auto simp: sorted_mid_iff2)
 
-lemma del_list_sorted2: "sorted (xs @ x # ys) \<Longrightarrow> y < x \<Longrightarrow>
-  del_list y (xs @ x # ys) = del_list y xs @ x # ys"
+lemma del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow>
+  del_list x (xs @ a # ys) = del_list x xs @ a # ys"
 by (induction xs) (auto simp: sorted_Cons_iff intro!: del_list_idem)
 
 lemma del_list_sorted3:
-  "sorted (xs @ x # ys @ y # zs) \<Longrightarrow> a < y \<Longrightarrow>
-  del_list a (xs @ x # ys @ y # zs) = del_list a (xs @ x # ys) @ y # zs"
+  "sorted (xs @ a # ys @ b # zs) \<Longrightarrow> x < b \<Longrightarrow>
+  del_list x (xs @ a # ys @ b # zs) = del_list x (xs @ a # ys) @ b # zs"
 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2)
 
 lemma del_list_sorted4:
-  "sorted (xs @ x # ys @ y # zs @ z # us) \<Longrightarrow> a < z \<Longrightarrow>
-  del_list a (xs @ x # ys @ y # zs @ z # us) = del_list a (xs @ x # ys @ y # zs) @ z # us"
+  "sorted (xs @ a # ys @ b # zs @ c # us) \<Longrightarrow> x < c \<Longrightarrow>
+  del_list x (xs @ a # ys @ b # zs @ c # us) = del_list x (xs @ a # ys @ b # zs) @ c # us"
 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3)
 
 lemma del_list_sorted5:
-  "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow>
-   del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) =
-   del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" 
+  "sorted (xs @ a # ys @ b # zs @ c # us @ d # vs) \<Longrightarrow> x < d \<Longrightarrow>
+   del_list x (xs @ a # ys @ b # zs @ c # us @ d # vs) =
+   del_list x (xs @ a # ys @ b # zs @ c # us) @ d # vs" 
 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
 
 lemmas del_list_simps = sorted_lems
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Data_Structures/RBT.thy
--- a/src/HOL/Data_Structures/RBT.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Data_Structures/RBT.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -27,23 +27,23 @@
 "red (Node _ l a r) = R l a r"
 
 fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"balL (R t1 x t2) s t3 = R (B t1 x t2) s t3" |
+"balL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
 "balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" |
 "balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (red t3))" |
 "balL t1 x t2 = R t1 x t2"
 
 fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
-"balR (B t1 x t2) y bl = bal (R t1 x t2) y bl" |
-"balR (R t1 x (B t2 y t3)) z bl = R (bal (red t1) x t2) y (B t3 z bl)" |
+"balR (B t1 x t2) y t3 = bal (R t1 x t2) y t3" |
+"balR (R t1 x (B t2 y t3)) z t4 = R (bal (red t1) x t2) y (B t3 z t4)" |
 "balR t1 x t2 = R t1 x t2"
 
 fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "combine Leaf t = t" |
 "combine t Leaf = t" |
-"combine (R a x b) (R c y d) = (case combine b c of
-    R b2 z c2 \<Rightarrow> (R (R a x b2) z (R c2 y d)) |
-    bc \<Rightarrow> R a x (R bc y d))" |
+"combine (R t1 a t2) (R t3 c t4) = (case combine t2 t3 of
+    R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
+    t23 \<Rightarrow> R t1 a (R t23 c t4))" |
 "combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of
     R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
     t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Data_Structures/Set_by_Ordered.thy
--- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -13,13 +13,13 @@
 fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
 fixes set :: "'s \<Rightarrow> 'a set"
 fixes invar :: "'s \<Rightarrow> bool"
-assumes "set empty = {}"
-assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)"
-assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)"
-assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}"
-assumes "invar empty"
-assumes "invar s \<Longrightarrow> invar(insert a s)"
-assumes "invar s \<Longrightarrow> invar(delete a s)"
+assumes set_empty:    "set empty = {}"
+assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
+assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
+assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
+assumes invar_empty:  "invar empty"
+assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
+assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
 
 locale Set_by_Ordered =
 fixes empty :: "'t"
@@ -30,14 +30,14 @@
 fixes wf :: "'t \<Rightarrow> bool"
 assumes empty: "inorder empty = []"
 assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow>
-  isin t a = (a \<in> elems (inorder t))"
+  isin t x = (x \<in> elems (inorder t))"
 assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow>
-  inorder(insert a t) = ins_list a (inorder t)"
+  inorder(insert x t) = ins_list x (inorder t)"
 assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
-  inorder(delete a t) = del_list a (inorder t)"
+  inorder(delete x t) = del_list x (inorder t)"
 assumes wf_empty:  "wf empty"
-assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)"
-assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)"
+assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert x t)"
+assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete x t)"
 begin
 
 sublocale Set
@@ -49,8 +49,8 @@
 next
   case 3 thus ?case by(simp add: insert)
 next
-  case (4 s a) show ?case
-    using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted)
+  case (4 s x) show ?case
+    using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted)
 next
   case 5 thus ?case by(simp add: empty wf_empty)
 next
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Data_Structures/Tree23_Map.thy
--- a/src/HOL/Data_Structures/Tree23_Map.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Map.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -21,53 +21,53 @@
    else lookup r x)"
 
 fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
-"upd a b Leaf = Up\<^sub>i Leaf (a,b) Leaf" |
-"upd a b (Node2 l xy r) =
-   (if a < fst xy then
-        (case upd a b l of
-           T\<^sub>i l' => T\<^sub>i (Node2 l' xy r)
-         | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 xy r))
-    else if a = fst xy then T\<^sub>i (Node2 l (a,b) r)
+"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
+"upd x y (Node2 l ab r) =
+   (if x < fst ab then
+        (case upd x y l of
+           T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
+         | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r))
+    else if x = fst ab then T\<^sub>i (Node2 l (x,y) r)
     else
-        (case upd a b r of
-           T\<^sub>i r' => T\<^sub>i (Node2 l xy r')
-         | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l xy r1 q r2)))" |
-"upd a b (Node3 l xy1 m xy2 r) =
-   (if a < fst xy1 then
-        (case upd a b l of
-           T\<^sub>i l' => T\<^sub>i (Node3 l' xy1 m xy2 r)
-         | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) xy1 (Node2 m xy2 r))
-    else if a = fst xy1 then T\<^sub>i (Node3 l (a,b) m xy2 r)
-    else if a < fst xy2 then
-             (case upd a b m of
-                T\<^sub>i m' => T\<^sub>i (Node3 l xy1 m' xy2 r)
-              | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l xy1 m1) q (Node2 m2 xy2 r))
-         else if a = fst xy2 then T\<^sub>i (Node3 l xy1 m (a,b) r)
+        (case upd x y r of
+           T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
+         | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" |
+"upd x y (Node3 l ab1 m ab2 r) =
+   (if x < fst ab1 then
+        (case upd x y l of
+           T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
+         | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r))
+    else if x = fst ab1 then T\<^sub>i (Node3 l (x,y) m ab2 r)
+    else if x < fst ab2 then
+             (case upd x y m of
+                T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
+              | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r))
+         else if x = fst ab2 then T\<^sub>i (Node3 l ab1 m (x,y) r)
          else
-             (case upd a b r of
-                T\<^sub>i r' => T\<^sub>i (Node3 l xy1 m xy2 r')
-              | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l xy1 m) xy2 (Node2 r1 q r2)))"
+             (case upd x y r of
+                T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
+              | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2)))"
 
 definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
 "update a b t = tree\<^sub>i(upd a b t)"
 
 fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d"
 where
-"del k Leaf = T\<^sub>d Leaf" |
-"del k (Node2 Leaf p Leaf) = (if k=fst p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
-"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=fst p then Node2 Leaf q Leaf
-  else if k=fst q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
-"del k (Node2 l a r) = (if k<fst a then node21 (del k l) a r else
-  if k > fst a then node22 l a (del k r) else
-  let (a',t) = del_min r in node22 l a' t)" |
-"del k (Node3 l a m b r) = (if k<fst a then node31 (del k l) a m b r else
-  if k = fst a then let (a',m') = del_min m in node32 l a' m' b r else
-  if k < fst b then node32 l a (del k m) b r else
-  if k = fst b then let (b',r') = del_min r in node33 l a m b' r'
-  else node33 l a m b (del k r))"
+"del x Leaf = T\<^sub>d Leaf" |
+"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
+"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
+  else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" |
+"del x (Node2 l ab1 r) = (if x<fst ab1 then node21 (del x l) ab1 r else
+  if x > fst ab1 then node22 l ab1 (del x r) else
+  let (ab1',t) = del_min r in node22 l ab1' t)" |
+"del x (Node3 l ab1 m ab2 r) = (if x<fst ab1 then node31 (del x l) ab1 m ab2 r else
+  if x = fst ab1 then let (ab1',m') = del_min m in node32 l ab1' m' ab2 r else
+  if x < fst ab2 then node32 l ab1 (del x m) ab2 r else
+  if x = fst ab2 then let (ab2',r') = del_min r in node33 l ab1 m ab2' r'
+  else node33 l ab1 m ab2 (del x r))"
 
 definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
-"delete k t = tree\<^sub>d(del k t)"
+"delete x t = tree\<^sub>d(del x t)"
 
 
 subsection \<open>Functional Correctness\<close>
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -12,7 +12,7 @@
 "isin Leaf x = False" |
 "isin (Node2 l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)" |
 "isin (Node3 l a m b r) x =
-  (x < a \<and> isin l x \<or> x = a \<or> (x < b \<and> isin m x \<or> x = b \<or> isin r x))"
+  (x < a \<and> isin l x \<or> x > b \<and> isin r x \<or> x = a \<or> x = b \<or> isin m x)"
 
 datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
 
@@ -21,37 +21,38 @@
 "tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
 
 fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
-"ins a Leaf = Up\<^sub>i Leaf a Leaf" |
-"ins a (Node2 l x r) =
-   (if a < x then
-      case ins a l of
-         T\<^sub>i l' => T\<^sub>i (Node2 l' x r)
-       | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 x r)
-    else if a=x then T\<^sub>i (Node2 l x r)
+"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
+"ins x (Node2 l a r) =
+   (if x < a then
+      case ins x l of
+         T\<^sub>i l' => T\<^sub>i (Node2 l' a r)
+       | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)
+    else if x=a then T\<^sub>i (Node2 l x r)
     else
-      case ins a r of
-        T\<^sub>i r' => T\<^sub>i (Node2 l x r')
-      | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l x r1 q r2))" |
-"ins a (Node3 l x1 m x2 r) =
-   (if a < x1 then
-      case ins a l of
-        T\<^sub>i l' => T\<^sub>i (Node3 l' x1 m x2 r)
-      | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) x1 (Node2 m x2 r)
-    else if a=x1 then T\<^sub>i (Node3 l x1 m x2 r)
-    else if a < x2 then
-           case ins a m of
-             T\<^sub>i m' => T\<^sub>i (Node3 l x1 m' x2 r)
-           | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l x1 m1) q (Node2 m2 x2 r)
-         else if a=x2 then T\<^sub>i (Node3 l x1 m x2 r)
-         else
-           case ins a r of
-             T\<^sub>i r' => T\<^sub>i (Node3 l x1 m x2 r')
-           | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l x1 m) x2 (Node2 r1 q r2))"
+      case ins x r of
+        T\<^sub>i r' => T\<^sub>i (Node2 l a r')
+      | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2))" |
+"ins x (Node3 l a m b r) =
+   (if x < a then
+      case ins x l of
+        T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r)
+      | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)
+    else
+    if x > b then
+      case ins x r of
+        T\<^sub>i r' => T\<^sub>i (Node3 l a m b r')
+      | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)
+    else
+    if x=a \<or> x = b then T\<^sub>i (Node3 l a m b r)
+    else
+      case ins x m of
+        T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r)
+      | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))"
 
 hide_const insert
 
 definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
-"insert a t = tree\<^sub>i(ins a t)"
+"insert x t = tree\<^sub>i(ins x t)"
 
 datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
 
@@ -94,21 +95,21 @@
 
 fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
 where
-"del k Leaf = T\<^sub>d Leaf" |
-"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
-"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
-  else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
-"del k (Node2 l a r) = (if k<a then node21 (del k l) a r else
-  if k > a then node22 l a (del k r) else
+"del x Leaf = T\<^sub>d Leaf" |
+"del x (Node2 Leaf a Leaf) = (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
+"del x (Node3 Leaf a Leaf b Leaf) = T\<^sub>d(if x = a then Node2 Leaf b Leaf
+  else if x = b then Node2 Leaf a Leaf else Node3 Leaf a Leaf b Leaf)" |
+"del x (Node2 l a r) = (if x<a then node21 (del x l) a r else
+  if x > a then node22 l a (del x r) else
   let (a',t) = del_min r in node22 l a' t)" |
-"del k (Node3 l a m b r) = (if k<a then node31 (del k l) a m b r else
-  if k = a then let (a',m') = del_min m in node32 l a' m' b r else
-  if k < b then node32 l a (del k m) b r else
-  if k = b then let (b',r') = del_min r in node33 l a m b' r'
-  else node33 l a m b (del k r))"
+"del x (Node3 l a m b r) = (if x<a then node31 (del x l) a m b r else
+  if x = a then let (a',m') = del_min m in node32 l a' m' b r else
+  if x < b then node32 l a (del x m) b r else
+  if x = b then let (b',r') = del_min r in node33 l a m b' r'
+  else node33 l a m b (del x r))"
 
 definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
-"delete k t = tree\<^sub>d(del k t)"
+"delete x t = tree\<^sub>d(del x t)"
 
 
 subsection "Functional Correctness"
@@ -127,7 +128,7 @@
 
 lemma inorder_ins:
   "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
-by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits)
+by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits) (* 38 secs in 2015 *)
 
 lemma inorder_insert:
   "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
@@ -194,7 +195,7 @@
 end
 
 lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
-by (induct t) (auto split: up\<^sub>i.split) (* 25 secs in 2015 *)
+by (induct t) (auto split: up\<^sub>i.split) (* 87 secs in 2015 *)
 
 text{* Now an alternative proof (by Brian Huffman) that runs faster because
 two properties (balance and height) are combined in one predicate. *}
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Data_Structures/Tree_Map.thy
--- a/src/HOL/Data_Structures/Tree_Map.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -14,16 +14,16 @@
   if x > a then lookup r x else Some b)"
 
 fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"update a b Leaf = Node Leaf (a,b) Leaf" |
-"update a b (Node l (x,y) r) =
-   (if a < x then Node (update a b l) (x,y) r
-    else if a=x then Node l (a,b) r
-    else Node l (x,y) (update a b r))"
+"update x y Leaf = Node Leaf (x,y) Leaf" |
+"update x y (Node l (a,b) r) =
+   (if x < a then Node (update x y l) (a,b) r
+    else if x = a then Node l (x,y) r
+    else Node l (a,b) (update x y r))"
 
 fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"delete k Leaf = Leaf" |
-"delete k (Node l (a,b) r) = (if k<a then Node (delete k l) (a,b) r else
-  if k > a then Node l (a,b) (delete k r) else
+"delete x Leaf = Leaf" |
+"delete x (Node l (a,b) r) = (if x < a then Node (delete x l) (a,b) r else
+  if x > a then Node l (a,b) (delete x r) else
   if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
 
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -15,20 +15,20 @@
 hide_const (open) insert
 
 fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"insert a Leaf = Node Leaf a Leaf" |
-"insert a (Node l x r) =
-   (if a < x then Node (insert a l) x r
-    else if a=x then Node l x r
-    else Node l x (insert a r))"
+"insert x Leaf = Node Leaf x Leaf" |
+"insert x (Node l a r) =
+   (if x < a then Node (insert x l) a r else
+    if x = a then Node l a r
+    else Node l a (insert x r))"
 
 fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
 "del_min (Node Leaf a r) = (a, r)" |
 "del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))"
 
 fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"delete k Leaf = Leaf" |
-"delete k (Node l a r) = (if k<a then Node (delete k l) a r else
-  if k > a then Node l a (delete k r) else
+"delete x Leaf = Leaf" |
+"delete x (Node l a r) = (if x < a then Node (delete x l) a r else
+  if x > a then Node l a (delete x r) else
   if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
 
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -11,14 +11,13 @@
 subsection \<open>Continuous linear forms\<close>
 
 text \<open>
-  A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
-  is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e.
+  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>,
+  iff it is bounded, i.e.
   \begin{center}
-  @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
-  In our application no other functions than linear forms are
-  considered, so we can define continuous linear forms as bounded
-  linear forms:
+  In our application no other functions than linear forms are considered, so
+  we can define continuous linear forms as bounded linear forms:
 \<close>
 
 locale continuous = linearform +
@@ -42,34 +41,31 @@
 subsection \<open>The norm of a linear form\<close>
 
 text \<open>
-  The least real number @{text c} for which holds
+  The least real number \<open>c\<close> for which holds
   \begin{center}
-  @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  \<open>\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
-  is called the \<^emph>\<open>norm\<close> of @{text f}.
+  is called the \<^emph>\<open>norm\<close> of \<open>f\<close>.
 
-  For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
-  defined as
+  For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as
   \begin{center}
-  @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
+  \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
   \end{center}
 
-  For the case @{text "V = {0}"} the supremum would be taken from an
-  empty set. Since @{text \<real>} is unbounded, there would be no supremum.
-  To avoid this situation it must be guaranteed that there is an
-  element in this set. This element must be @{text "{} \<ge> 0"} so that
-  @{text fn_norm} has the norm properties. Furthermore it does not
-  have to change the norm in all other cases, so it must be @{text 0},
-  as all other elements are @{text "{} \<ge> 0"}.
+  For the case \<open>V = {0}\<close> the supremum would be taken from an empty set.
+  Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this
+  situation it must be guaranteed that there is an element in this set. This
+  element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties.
+  Furthermore it does not have to change the norm in all other cases, so it
+  must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>.
 
-  Thus we define the set @{text B} where the supremum is taken from as
-  follows:
+  Thus we define the set \<open>B\<close> where the supremum is taken from as follows:
   \begin{center}
-  @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
+  \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
   \end{center}
 
-  @{text fn_norm} is equal to the supremum of @{text B}, if the
-  supremum exists (otherwise it is undefined).
+  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists
+  (otherwise it is undefined).
 \<close>
 
 locale fn_norm =
@@ -84,8 +80,8 @@
   by (simp add: B_def)
 
 text \<open>
-  The following lemma states that every continuous linear form on a
-  normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
+  The following lemma states that every continuous linear form on a normed
+  space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
 \<close>
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
@@ -98,19 +94,19 @@
     non-empty bounded set of reals has a supremum.\<close>
   have "\<exists>a. lub (B V f) a"
   proof (rule real_complete)
-    txt \<open>First we have to show that @{text B} is non-empty:\<close>
+    txt \<open>First we have to show that \<open>B\<close> is non-empty:\<close>
     have "0 \<in> B V f" ..
     then show "\<exists>x. x \<in> B V f" ..
 
-    txt \<open>Then we have to show that @{text B} is bounded:\<close>
+    txt \<open>Then we have to show that \<open>B\<close> is bounded:\<close>
     show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
     proof -
-      txt \<open>We know that @{text f} is bounded by some value @{text c}.\<close>
+      txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close>
       from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
 
-      txt \<open>To prove the thesis, we have to show that there is some
-        @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
-        B"}. Due to the definition of @{text B} there are two cases.\<close>
+      txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such
+        that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are
+        two cases.\<close>
 
       def b \<equiv> "max c 0"
       have "\<forall>y \<in> B V f. y \<le> b"
@@ -121,8 +117,8 @@
           assume "y = 0"
           then show ?thesis unfolding b_def by arith
         next
-          txt \<open>The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
-            @{text "x \<in> V"} with @{text "x \<noteq> 0"}.\<close>
+          txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some
+            \<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<close>
           assume "y \<noteq> 0"
           with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
               and x: "x \<in> V" and neq: "x \<noteq> 0"
@@ -130,7 +126,7 @@
           from x neq have gt: "0 < \<parallel>x\<parallel>" ..
 
           txt \<open>The thesis follows by a short calculation using the
-            fact that @{text f} is bounded.\<close>
+            fact that \<open>f\<close> is bounded.\<close>
 
           note y_rep
           also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
@@ -177,16 +173,16 @@
   from this and b show ?thesis ..
 qed
 
-text \<open>The norm of a continuous function is always @{text "\<ge> 0"}.\<close>
+text \<open>The norm of a continuous function is always \<open>\<ge> 0\<close>.\<close>
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
   assumes "continuous V f norm"
   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
   interpret continuous V f norm by fact
-  txt \<open>The function norm is defined as the supremum of @{text B}.
-    So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
-    0"}, provided the supremum exists and @{text B} is not empty.\<close>
+  txt \<open>The function norm is defined as the supremum of \<open>B\<close>.
+    So it is \<open>\<ge> 0\<close> if all elements in \<open>B\<close> are \<open>\<ge>
+    0\<close>, provided the supremum exists and \<open>B\<close> is not empty.\<close>
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
     using \<open>continuous V f norm\<close> by (rule fn_norm_works)
   moreover have "0 \<in> B V f" ..
@@ -197,7 +193,7 @@
   \<^medskip>
   The fundamental property of function norms is:
   \begin{center}
-  @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+  \<open>\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
 \<close>
 
@@ -237,10 +233,10 @@
 
 text \<open>
   \<^medskip>
-  The function norm is the least positive real number for
-  which the following inequation holds:
+  The function norm is the least positive real number for which the
+  following inequality holds:
   \begin{center}
-    @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+    \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   \end{center}
 \<close>
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Function_Order.thy
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -11,10 +11,10 @@
 subsection \<open>The graph of a function\<close>
 
 text \<open>
-  We define the \<^emph>\<open>graph\<close> of a (real) function @{text f} with
-  domain @{text F} as the set
+  We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with
+  domain \<open>F\<close> as the set
   \begin{center}
-  @{text "{(x, f x). x \<in> F}"}
+  \<open>{(x, f x). x \<in> F}\<close>
   \end{center}
   So we are modeling partial functions by specifying the domain and
   the mapping function. We use the term ``function'' also for its
@@ -41,8 +41,8 @@
 subsection \<open>Functions ordered by domain extension\<close>
 
 text \<open>
-  A function @{text h'} is an extension of @{text h}, iff the graph of
-  @{text h} is a subset of the graph of @{text h'}.
+  A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of
+  \<open>h\<close> is a subset of the graph of \<open>h'\<close>.
 \<close>
 
 lemma graph_extI:
@@ -60,8 +60,7 @@
 subsection \<open>Domain and function of a graph\<close>
 
 text \<open>
-  The inverse functions to @{text graph} are @{text domain} and @{text
-  funct}.
+  The inverse functions to \<open>graph\<close> are \<open>domain\<close> and \<open>funct\<close>.
 \<close>
 
 definition domain :: "'a graph \<Rightarrow> 'a set"
@@ -71,8 +70,8 @@
   where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
 
 text \<open>
-  The following lemma states that @{text g} is the graph of a function
-  if the relation induced by @{text g} is unique.
+  The following lemma states that \<open>g\<close> is the graph of a function if the
+  relation induced by \<open>g\<close> is unique.
 \<close>
 
 lemma graph_domain_funct:
@@ -94,10 +93,9 @@
 subsection \<open>Norm-preserving extensions of a function\<close>
 
 text \<open>
-  Given a linear form @{text f} on the space @{text F} and a seminorm
-  @{text p} on @{text E}. The set of all linear extensions of @{text
-  f}, to superspaces @{text H} of @{text F}, which are bounded by
-  @{text p}, is defined as follows.
+  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The
+  set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
+  bounded by \<open>p\<close>, is defined as follows.
 \<close>
 
 definition
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -9,42 +9,39 @@
 begin
 
 text \<open>
-  We present the proof of two different versions of the Hahn-Banach
-  Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
+  We present the proof of two different versions of the Hahn-Banach Theorem,
+  closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
 \<close>
 
+
 subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
 
 paragraph \<open>Hahn-Banach Theorem.\<close>
 text \<open>
-  Let @{text F} be a subspace of a real vector space @{text E}, let @{text
-  p} be a semi-norm on @{text E}, and @{text f} be a linear form defined on
-  @{text F} such that @{text f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in>
-  F. f x \<le> p x"}. Then @{text f} can be extended to a linear form @{text h}
-  on @{text E} such that @{text h} is norm-preserving, i.e. @{text h} is
-  also bounded by @{text p}.
+  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
+  on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded
+  by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear
+  form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded
+  by \<open>p\<close>.
 \<close>
 
 paragraph \<open>Proof Sketch.\<close>
 text \<open>
-  \<^enum> Define @{text M} as the set of norm-preserving extensions of
-  @{text f} to subspaces of @{text E}. The linear forms in @{text M}
-  are ordered by domain extension.
+  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
+  of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
 
-  \<^enum> We show that every non-empty chain in @{text M} has an upper
-  bound in @{text M}.
+  \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
+
+  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in
+  \<open>M\<close>.
 
-  \<^enum> With Zorn's Lemma we conclude that there is a maximal function
-  @{text g} in @{text M}.
-
-  \<^enum> The domain @{text H} of @{text g} is the whole space @{text
-  E}, as shown by classical contradiction:
+  \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
+  contradiction:
 
-    \<^item> Assuming @{text g} is not defined on whole @{text E}, it can
-    still be extended in a norm-preserving way to a super-space @{text
-    H'} of @{text H}.
+    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in
+    a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
 
-    \<^item> Thus @{text g} can not be maximal. Contradiction!
+    \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
 \<close>
 
 theorem Hahn_Banach:
@@ -52,9 +49,9 @@
     and "seminorm E p" and "linearform F f"
   assumes fp: "\<forall>x \<in> F. f x \<le> p x"
   shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
-    -- \<open>Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E},\<close>
-    -- \<open>and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p},\<close>
-    -- \<open>then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \<^smallskip>\<close>
+    -- \<open>Let \<open>E\<close> be a vector space, \<open>F\<close> a subspace of \<open>E\<close>, \<open>p\<close> a seminorm on \<open>E\<close>,\<close>
+    -- \<open>and \<open>f\<close> a linear form on \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>,\<close>
+    -- \<open>then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> in a norm-preserving way. \<^smallskip>\<close>
 proof -
   interpret vectorspace E by fact
   interpret subspace F E by fact
@@ -67,8 +64,8 @@
   {
     fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c"
     have "\<Union>c \<in> M"
-      -- \<open>Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}:\<close>
-      -- \<open>@{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}.\<close>
+      -- \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close>
+      -- \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close>
       unfolding M_def
     proof (rule norm_pres_extensionI)
       let ?H = "domain (\<Union>c)"
@@ -98,9 +95,9 @@
     qed
   }
   then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
-  -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \<^smallskip>\<close>
+  -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in \<open>M\<close>. \<^smallskip>\<close>
   proof (rule Zorn's_Lemma)
-      -- \<open>We show that @{text M} is non-empty:\<close>
+      -- \<open>We show that \<open>M\<close> is non-empty:\<close>
     show "graph F f \<in> M"
       unfolding M_def
     proof (rule norm_pres_extensionI2)
@@ -119,18 +116,18 @@
     and HE: "H \<unlhd> E" and FH: "F \<unlhd> H"
     and graphs: "graph F f \<subseteq> graph H h"
     and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def ..
-      -- \<open>@{text g} is a norm-preserving extension of @{text f}, in other words:\<close>
-      -- \<open>@{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E},\<close>
-      -- \<open>and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \<^smallskip>\<close>
+      -- \<open>\<open>g\<close> is a norm-preserving extension of \<open>f\<close>, in other words:\<close>
+      -- \<open>\<open>g\<close> is the graph of some linear form \<open>h\<close> defined on a subspace \<open>H\<close> of \<open>E\<close>,\<close>
+      -- \<open>and \<open>h\<close> is an extension of \<open>f\<close> that is again bounded by \<open>p\<close>. \<^smallskip>\<close>
   from HE E have H: "vectorspace H"
     by (rule subspace.vectorspace)
 
   have HE_eq: "H = E"
-    -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \<^smallskip>\<close>
+    -- \<open>We show that \<open>h\<close> is defined on whole \<open>E\<close> by classical contradiction. \<^smallskip>\<close>
   proof (rule classical)
     assume neq: "H \<noteq> E"
-      -- \<open>Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended\<close>
-      -- \<open>in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \<^smallskip>\<close>
+      -- \<open>Assume \<open>h\<close> is not defined on whole \<open>E\<close>. Then show that \<open>h\<close> can be extended\<close>
+      -- \<open>in a norm-preserving way to a function \<open>h'\<close> with the graph \<open>g'\<close>. \<^smallskip>\<close>
     have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
     proof -
       from HE have "H \<subseteq> E" ..
@@ -146,7 +143,7 @@
       qed
 
       def H' \<equiv> "H + lin x'"
-        -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \<^smallskip>\<close>
+        -- \<open>Define \<open>H'\<close> as the direct sum of \<open>H\<close> and the linear closure of \<open>x'\<close>. \<^smallskip>\<close>
       have HH': "H \<unlhd> H'"
       proof (unfold H'_def)
         from x'E have "vectorspace (lin x')" ..
@@ -156,8 +153,8 @@
       obtain xi where
         xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
           \<and> xi \<le> p (y + x') - h y"
-        -- \<open>Pick a real number @{text \<xi>} that fulfills certain inequations; this will\<close>
-        -- \<open>be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
+        -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
+        -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
            \label{ex-xi-use}\<^smallskip>\<close>
       proof -
         from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
@@ -185,10 +182,10 @@
 
       def h' \<equiv> "\<lambda>x. let (y, a) =
           SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi"
-        -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \<^smallskip>\<close>
+        -- \<open>Define the extension \<open>h'\<close> of \<open>h\<close> to \<open>H'\<close> using \<open>\<xi>\<close>. \<^smallskip>\<close>
 
       have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
-        -- \<open>@{text h'} is an extension of @{text h} \dots \<^smallskip>\<close>
+        -- \<open>\<open>h'\<close> is an extension of \<open>h\<close> \dots \<^smallskip>\<close>
       proof
         show "g \<subseteq> graph H' h'"
         proof -
@@ -225,7 +222,7 @@
         qed
       qed
       moreover have "graph H' h' \<in> M"
-        -- \<open>and @{text h'} is norm-preserving. \<^smallskip>\<close>
+        -- \<open>and \<open>h'\<close> is norm-preserving. \<^smallskip>\<close>
       proof (unfold M_def)
         show "graph H' h' \<in> norm_pres_extensions E p F f"
         proof (rule norm_pres_extensionI2)
@@ -273,7 +270,7 @@
       ultimately show ?thesis ..
     qed
     then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
-      -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \<^smallskip>\<close>
+      -- \<open>So the graph \<open>g\<close> of \<open>h\<close> cannot be maximal. Contradiction! \<^smallskip>\<close>
     with gx show "H = E" by contradiction
   qed
 
@@ -295,14 +292,14 @@
 
 text \<open>
   The following alternative formulation of the Hahn-Banach
-  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear
-  form @{text f} and a seminorm @{text p} the following inequations
-  are equivalent:\footnote{This was shown in lemma @{thm [source]
-  abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
+  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form
+  \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are
+  equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff}
+  (see page \pageref{abs-ineq-iff}).}
   \begin{center}
   \begin{tabular}{lll}
-  @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
-  @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
+  \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
   \end{tabular}
   \end{center}
 \<close>
@@ -339,9 +336,9 @@
 subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
 
 text \<open>
-  Every continuous linear form @{text f} on a subspace @{text F} of a
-  norm space @{text E}, can be extended to a continuous linear form
-  @{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}.
+  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>,
+  can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> =
+  \<parallel>g\<parallel>\<close>.
 \<close>
 
 theorem norm_Hahn_Banach:
@@ -370,22 +367,22 @@
     by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
       [OF normed_vectorspace_with_fn_norm.intro,
        OF F_norm \<open>continuous F f norm\<close> , folded B_def fn_norm_def])
-  txt \<open>We define a function @{text p} on @{text E} as follows:
-    @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}\<close>
+  txt \<open>We define a function \<open>p\<close> on \<open>E\<close> as follows:
+    \<open>p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>\<close>
   def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
 
-  txt \<open>@{text p} is a seminorm on @{text E}:\<close>
+  txt \<open>\<open>p\<close> is a seminorm on \<open>E\<close>:\<close>
   have q: "seminorm E p"
   proof
     fix x y a assume x: "x \<in> E" and y: "y \<in> E"
     
-    txt \<open>@{text p} is positive definite:\<close>
+    txt \<open>\<open>p\<close> is positive definite:\<close>
     have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
     moreover from x have "0 \<le> \<parallel>x\<parallel>" ..
     ultimately show "0 \<le> p x"  
       by (simp add: p_def zero_le_mult_iff)
 
-    txt \<open>@{text p} is absolutely homogeneous:\<close>
+    txt \<open>\<open>p\<close> is absolutely homogeneous:\<close>
 
     show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
     proof -
@@ -396,7 +393,7 @@
       finally show ?thesis .
     qed
 
-    txt \<open>Furthermore, @{text p} is subadditive:\<close>
+    txt \<open>Furthermore, \<open>p\<close> is subadditive:\<close>
 
     show "p (x + y) \<le> p x + p y"
     proof -
@@ -411,7 +408,7 @@
     qed
   qed
 
-  txt \<open>@{text f} is bounded by @{text p}.\<close>
+  txt \<open>\<open>f\<close> is bounded by \<open>p\<close>.\<close>
 
   have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   proof
@@ -423,10 +420,10 @@
          OF F_norm, folded B_def fn_norm_def])
   qed
 
-  txt \<open>Using the fact that @{text p} is a seminorm and @{text f} is bounded
-    by @{text p} we can apply the Hahn-Banach Theorem for real vector
-    spaces. So @{text f} can be extended in a norm-preserving way to
-    some function @{text g} on the whole vector space @{text E}.\<close>
+  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we
+    can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
+    extended in a norm-preserving way to some function \<open>g\<close> on the whole
+    vector space \<open>E\<close>.\<close>
 
   with E FE linearform q obtain g where
       linearformE: "linearform E g"
@@ -434,7 +431,7 @@
     and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
     by (rule abs_Hahn_Banach [elim_format]) iprover
 
-  txt \<open>We furthermore have to show that @{text g} is also continuous:\<close>
+  txt \<open>We furthermore have to show that \<open>g\<close> is also continuous:\<close>
 
   have g_cont: "continuous E g norm" using linearformE
   proof
@@ -443,25 +440,25 @@
       by (simp only: p_def)
   qed
 
-  txt \<open>To complete the proof, we show that @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}.\<close>
+  txt \<open>To complete the proof, we show that \<open>\<parallel>g\<parallel> = \<parallel>f\<parallel>\<close>.\<close>
 
   have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
   proof (rule order_antisym)
     txt \<open>
-      First we show @{text "\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>"}.  The function norm @{text
-      "\<parallel>g\<parallel>"} is defined as the smallest @{text "c \<in> \<real>"} such that
+      First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the
+      smallest \<open>c \<in> \<real>\<close> such that
       \begin{center}
       \begin{tabular}{l}
-      @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+      \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
       \end{tabular}
       \end{center}
-      \noindent Furthermore holds
+      \<^noindent> Furthermore holds
       \begin{center}
       \begin{tabular}{l}
-      @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+      \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
       \end{tabular}
       \end{center}
-\<close>
+    \<close>
 
     from g_cont _ ge_zero
     show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -9,34 +9,30 @@
 begin
 
 text \<open>
-  In this section the following context is presumed.  Let @{text E} be
-  a real vector space with a seminorm @{text q} on @{text E}. @{text
-  F} is a subspace of @{text E} and @{text f} a linear function on
-  @{text F}. We consider a subspace @{text H} of @{text E} that is a
-  superspace of @{text F} and a linear form @{text h} on @{text
-  H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is
-  an element in @{text "E - H"}.  @{text H} is extended to the direct
-  sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}
-  the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is
-  unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
-  a \<cdot> \<xi>"} for a certain @{text \<xi>}.
+  In this section the following context is presumed. Let \<open>E\<close> be a real
+  vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close>
+  a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
+  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close>
+  and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H'
+  = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close>
+  with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close>
+  for a certain \<open>\<xi>\<close>.
 
-  Subsequently we show some properties of this extension @{text h'} of
-  @{text h}.
+  Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.
 
   \<^medskip>
-  This lemma will be used to show the existence of a linear
-  extension of @{text f} (see page \pageref{ex-xi-use}). It is a
-  consequence of the completeness of @{text \<real>}. To show
+  This lemma will be used to show the existence of a linear extension of \<open>f\<close>
+  (see page \pageref{ex-xi-use}). It is a consequence of the completeness of
+  \<open>\<real>\<close>. To show
   \begin{center}
   \begin{tabular}{l}
-  @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}
+  \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close>
   \end{tabular}
   \end{center}
-  \noindent it suffices to show that
+  \<^noindent> it suffices to show that
   \begin{center}
   \begin{tabular}{l}
-  @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
+  \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>
   \end{tabular}
   \end{center}
 \<close>
@@ -48,7 +44,7 @@
 proof -
   interpret vectorspace F by fact
   txt \<open>From the completeness of the reals follows:
-    The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
+    The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is
     non-empty and has an upper bound.\<close>
 
   let ?S = "{a u | u. u \<in> F}"
@@ -86,9 +82,8 @@
 
 text \<open>
   \<^medskip>
-  The function @{text h'} is defined as a @{text "h' x = h y
-  + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
-  @{text h} to @{text H'}.
+  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where
+  \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>.
 \<close>
 
 lemma h'_lf:
@@ -194,8 +189,8 @@
 
 text \<open>
   \<^medskip>
-  The linear extension @{text h'} of @{text h}
-  is bounded by the seminorm @{text p}.\<close>
+  The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>.
+\<close>
 
 lemma h'_norm_pres:
   assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
@@ -235,8 +230,8 @@
         also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
         finally show ?thesis .
       next
-        txt \<open>In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
-          with @{text ya} taken as @{text "y / a"}:\<close>
+        txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close>
+          with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>
         assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
         from a1 ay
         have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
@@ -257,8 +252,8 @@
         finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
         then show ?thesis by simp
       next
-        txt \<open>In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
-          with @{text ya} taken as @{text "y / a"}:\<close>
+        txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close>
+          with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>
         assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
         from a2 ay
         have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -2,27 +2,25 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
-section \<open>The supremum w.r.t.~the function order\<close>
+section \<open>The supremum wrt.\ the function order\<close>
 
 theory Hahn_Banach_Sup_Lemmas
 imports Function_Norm Zorn_Lemma
 begin
 
 text \<open>
-  This section contains some lemmas that will be used in the proof of
-  the Hahn-Banach Theorem.  In this section the following context is
-  presumed.  Let @{text E} be a real vector space with a seminorm
-  @{text p} on @{text E}.  @{text F} is a subspace of @{text E} and
-  @{text f} a linear form on @{text F}. We consider a chain @{text c}
-  of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
-  graph H h"}.  We will show some properties about the limit function
-  @{text h}, i.e.\ the supremum of the chain @{text c}.
+  This section contains some lemmas that will be used in the proof of the
+  Hahn-Banach Theorem. In this section the following context is presumed.
+  Let \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a
+  subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of
+  norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will
+  show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of
+  the chain \<open>c\<close>.
 
   \<^medskip>
-  Let @{text c} be a chain of norm-preserving extensions of
-  the function @{text f} and let @{text "graph H h"} be the supremum
-  of @{text c}.  Every element in @{text H} is member of one of the
-  elements of the chain.
+  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
+  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of
+  one of the elements of the chain.
 \<close>
 
 lemmas [dest?] = chainsD
@@ -57,11 +55,10 @@
 
 text \<open>
   \<^medskip>
-  Let @{text c} be a chain of norm-preserving extensions of
-  the function @{text f} and let @{text "graph H h"} be the supremum
-  of @{text c}.  Every element in the domain @{text H} of the supremum
-  function is member of the domain @{text H'} of some function @{text
-  h'}, such that @{text h} extends @{text h'}.
+  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
+  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of
+  the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>,
+  such that \<open>h\<close> extends \<open>h'\<close>.
 \<close>
 
 lemma some_H'h':
@@ -86,10 +83,9 @@
 
 text \<open>
   \<^medskip>
-  Any two elements @{text x} and @{text y} in the domain
-  @{text H} of the supremum function @{text h} are both in the domain
-  @{text H'} of some function @{text h'}, such that @{text h} extends
-  @{text h'}.
+  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function
+  \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close>
+  extends \<open>h'\<close>.
 \<close>
 
 lemma some_H'h'2:
@@ -103,8 +99,8 @@
     \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
     \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
 proof -
-  txt \<open>@{text y} is in the domain @{text H''} of some function @{text h''},
-  such that @{text h} extends @{text h''}.\<close>
+  txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>,
+  such that \<open>h\<close> extends \<open>h''\<close>.\<close>
 
   from M cM u and y obtain H' h' where
       y_hy: "(y, h y) \<in> graph H' h'"
@@ -114,8 +110,8 @@
       "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
     by (rule some_H'h't [elim_format]) blast
 
-  txt \<open>@{text x} is in the domain @{text H'} of some function @{text h'},
-    such that @{text h} extends @{text h'}.\<close>
+  txt \<open>\<open>x\<close> is in the domain \<open>H'\<close> of some function \<open>h'\<close>,
+    such that \<open>h\<close> extends \<open>h'\<close>.\<close>
 
   from M cM u and x obtain H'' h'' where
       x_hx: "(x, h x) \<in> graph H'' h''"
@@ -125,9 +121,9 @@
       "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
     by (rule some_H'h't [elim_format]) blast
 
-  txt \<open>Since both @{text h'} and @{text h''} are elements of the chain,
-    @{text h''} is an extension of @{text h'} or vice versa. Thus both
-    @{text x} and @{text y} are contained in the greater
+  txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain,
+    \<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both
+    \<open>x\<close> and \<open>y\<close> are contained in the greater
     one. \label{cases1}\<close>
 
   from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
@@ -159,8 +155,8 @@
 
 text \<open>
   \<^medskip>
-  The relation induced by the graph of the supremum of a
-  chain @{text c} is definite, i.~e.~t is the graph of a function.
+  The relation induced by the graph of the supremum of a chain \<open>c\<close> is
+  definite, i.e.\ it is the graph of a function.
 \<close>
 
 lemma sup_definite:
@@ -182,9 +178,8 @@
   then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
     unfolding M_def by blast
 
-  txt \<open>@{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
-    or vice versa, since both @{text "G\<^sub>1"} and @{text
-    "G\<^sub>2"} are members of @{text c}. \label{cases2}\<close>
+  txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close>
+    are members of \<open>c\<close>. \label{cases2}\<close>
 
   from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
     by (blast dest: chainsD)
@@ -210,12 +205,11 @@
 
 text \<open>
   \<^medskip>
-  The limit function @{text h} is linear. Every element
-  @{text x} in the domain of @{text h} is in the domain of a function
-  @{text h'} in the chain of norm preserving extensions.  Furthermore,
-  @{text h} is an extension of @{text h'} so the function values of
-  @{text x} are identical for @{text h'} and @{text h}.  Finally, the
-  function @{text h'} is linear by construction of @{text M}.
+  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close>
+  is in the domain of a function \<open>h'\<close> in the chain of norm preserving
+  extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function
+  values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close>
+  is linear by construction of \<open>M\<close>.
 \<close>
 
 lemma sup_lf:
@@ -266,10 +260,9 @@
 
 text \<open>
   \<^medskip>
-  The limit of a non-empty chain of norm preserving
-  extensions of @{text f} is an extension of @{text f}, since every
-  element of the chain is an extension of @{text f} and the supremum
-  is an extension for every element of the chain.
+  The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an
+  extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close>
+  and the supremum is an extension for every element of the chain.
 \<close>
 
 lemma sup_ext:
@@ -293,10 +286,9 @@
 
 text \<open>
   \<^medskip>
-  The domain @{text H} of the limit function is a superspace
-  of @{text F}, since @{text F} is a subset of @{text H}. The
-  existence of the @{text 0} element in @{text F} and the closure
-  properties follow from the fact that @{text F} is a vector space.
+  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is
+  a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
+  properties follow from the fact that \<open>F\<close> is a vector space.
 \<close>
 
 lemma sup_supF:
@@ -319,8 +311,7 @@
 
 text \<open>
   \<^medskip>
-  The domain @{text H} of the limit function is a subspace of
-  @{text E}.
+  The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.
 \<close>
 
 lemma sup_subE:
@@ -376,8 +367,8 @@
 
 text \<open>
   \<^medskip>
-  The limit function is bounded by the norm @{text p} as
-  well, since all elements in the chain are bounded by @{text p}.
+  The limit function is bounded by the norm \<open>p\<close> as well, since all elements
+  in the chain are bounded by \<open>p\<close>.
 \<close>
 
 lemma sup_norm_pres:
@@ -398,14 +389,14 @@
 
 text \<open>
   \<^medskip>
-  The following lemma is a property of linear forms on real
-  vector spaces. It will be used for the lemma @{text abs_Hahn_Banach}
-  (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
-  vector spaces the following inequations are equivalent:
+  The following lemma is a property of linear forms on real vector spaces.
+  It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
+  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces
+  the following inequality are equivalent:
   \begin{center}
   \begin{tabular}{lll}
-  @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
-  @{text "\<forall>x \<in> H. h x \<le> p x"} \\
+  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
+  \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
   \end{tabular}
   \end{center}
 \<close>
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Linearform.thy
--- a/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Linearform.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -9,8 +9,8 @@
 begin
 
 text \<open>
-  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals
-  that is additive and multiplicative.
+  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
+  additive and multiplicative.
 \<close>
 
 locale linearform =
@@ -44,7 +44,7 @@
   finally show ?thesis by simp
 qed
 
-text \<open>Every linear form yields @{text 0} for the @{text 0} vector.\<close>
+text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close>
 
 lemma (in linearform) zero [iff]:
   assumes "vectorspace V"
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -11,9 +11,9 @@
 subsection \<open>Quasinorms\<close>
 
 text \<open>
-  A \<^emph>\<open>seminorm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
-  into the reals that has the following properties: it is positive
-  definite, absolute homogeneous and subadditive.
+  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals
+  that has the following properties: it is positive definite, absolute
+  homogeneous and subadditive.
 \<close>
 
 locale seminorm =
@@ -57,8 +57,8 @@
 subsection \<open>Norms\<close>
 
 text \<open>
-  A \<^emph>\<open>norm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
-  @{text 0} vector to @{text 0}.
+  A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the
+  \<open>0\<close> vector to \<open>0\<close>.
 \<close>
 
 locale norm = seminorm +
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -11,9 +11,8 @@
 subsection \<open>Definition\<close>
 
 text \<open>
-  A non-empty subset @{text U} of a vector space @{text V} is a
-  \<^emph>\<open>subspace\<close> of @{text V}, iff @{text U} is closed under addition
-  and scalar multiplication.
+  A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff
+  \<open>U\<close> is closed under addition and scalar multiplication.
 \<close>
 
 locale subspace =
@@ -51,9 +50,9 @@
 
 text \<open>
   \<^medskip>
-  Similar as for linear spaces, the existence of the zero
-  element in every subspace follows from the non-emptiness of the
-  carrier set and by vector space laws.
+  Similar as for linear spaces, the existence of the zero element in every
+  subspace follows from the non-emptiness of the carrier set and by vector
+  space laws.
 \<close>
 
 lemma (in subspace) zero [intro]:
@@ -140,8 +139,8 @@
 subsection \<open>Linear closure\<close>
 
 text \<open>
-  The \<^emph>\<open>linear closure\<close> of a vector @{text x} is the set of all
-  scalar multiples of @{text x}.
+  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples
+  of \<open>x\<close>.
 \<close>
 
 definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
@@ -227,8 +226,8 @@
 subsection \<open>Sum of two vectorspaces\<close>
 
 text \<open>
-  The \<^emph>\<open>sum\<close> of two vectorspaces @{text U} and @{text V} is the
-  set of all sums of elements from @{text U} and @{text V}.
+  The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the set of all sums of
+  elements from \<open>U\<close> and \<open>V\<close>.
 \<close>
 
 lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}"
@@ -246,7 +245,7 @@
     "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
   unfolding sum_def by blast
 
-text \<open>@{text U} is a subspace of @{text "U + V"}.\<close>
+text \<open>\<open>U\<close> is a subspace of \<open>U + V\<close>.\<close>
 
 lemma subspace_sum1 [iff]:
   assumes "vectorspace U" "vectorspace V"
@@ -329,11 +328,10 @@
 subsection \<open>Direct sums\<close>
 
 text \<open>
-  The sum of @{text U} and @{text V} is called \<^emph>\<open>direct\<close>, iff the
-  zero element is the only common element of @{text U} and @{text
-  V}. For every element @{text x} of the direct sum of @{text U} and
-  @{text V} the decomposition in @{text "x = u + v"} with
-  @{text "u \<in> U"} and @{text "v \<in> V"} is unique.
+  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the
+  only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct
+  sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and
+  \<open>v \<in> V\<close> is unique.
 \<close>
 
 lemma decomp:
@@ -378,12 +376,10 @@
 qed
 
 text \<open>
-  An application of the previous lemma will be used in the proof of
-  the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
-  element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
-  vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
-  the components @{text "y \<in> H"} and @{text a} are uniquely
-  determined.
+  An application of the previous lemma will be used in the proof of the
+  Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any element
+  \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a vectorspace \<open>H\<close> and the linear closure
+  of \<open>x\<^sub>0\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely determined.
 \<close>
 
 lemma decomp_H':
@@ -437,10 +433,9 @@
 qed
 
 text \<open>
-  Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
-  vectorspace @{text H} and the linear closure of @{text x'} the
-  components @{text "y \<in> H"} and @{text a} are unique, it follows from
-  @{text "y \<in> H"} that @{text "a = 0"}.
+  Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close>
+  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique,
+  it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
 \<close>
 
 lemma decomp_H'_H:
@@ -465,9 +460,8 @@
 qed
 
 text \<open>
-  The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
-  are unique, so the function @{text h'} defined by
-  @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.
+  The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> are unique, so the function
+  \<open>h'\<close> defined by \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
 \<close>
 
 lemma h'_definite:
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -11,9 +11,9 @@
 subsection \<open>Signature\<close>
 
 text \<open>
-  For the definition of real vector spaces a type @{typ 'a} of the
-  sort @{text "{plus, minus, zero}"} is considered, on which a real
-  scalar multiplication @{text \<cdot>} is declared.
+  For the definition of real vector spaces a type @{typ 'a} of the sort
+  \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication
+  \<open>\<cdot>\<close> is declared.
 \<close>
 
 consts
@@ -23,14 +23,13 @@
 subsection \<open>Vector space laws\<close>
 
 text \<open>
-  A \<^emph>\<open>vector space\<close> is a non-empty set @{text V} of elements from
-  @{typ 'a} with the following vector space laws: The set @{text V} is
-  closed under addition and scalar multiplication, addition is
-  associative and commutative; @{text "- x"} is the inverse of @{text
-  x} w.~r.~t.~addition and @{text 0} is the neutral element of
-  addition.  Addition and multiplication are distributive; scalar
-  multiplication is associative and the real number @{text "1"} is
-  the neutral element of scalar multiplication.
+  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with
+  the following vector space laws: The set \<open>V\<close> is closed under addition and
+  scalar multiplication, addition is associative and commutative; \<open>- x\<close> is
+  the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of
+  addition. Addition and multiplication are distributive; scalar
+  multiplication is associative and the real number \<open>1\<close> is the neutral
+  element of scalar multiplication.
 \<close>
 
 locale vectorspace =
@@ -65,7 +64,8 @@
 lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
   by (simp add: negate_eq1)
 
-lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
+lemma add_left_commute:
+  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
 proof -
   assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"
   then have "x + (y + z) = (x + y) + z"
@@ -78,8 +78,8 @@
 lemmas add_ac = add_assoc add_commute add_left_commute
 
 
-text \<open>The existence of the zero element of a vector space
-  follows from the non-emptiness of carrier set.\<close>
+text \<open>The existence of the zero element of a vector space follows from the
+  non-emptiness of carrier set.\<close>
 
 lemma zero [iff]: "0 \<in> V"
 proof -
@@ -214,7 +214,8 @@
   then show "x + y = x + z" by (simp only:)
 qed
 
-lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
+lemma add_right_cancel:
+    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
   by (simp only: add_commute add_left_cancel)
 
 lemma add_assoc_cong:
@@ -372,4 +373,3 @@
 end
 
 end
-
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/Zorn_Lemma.thy
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -10,13 +10,12 @@
 
 text \<open>
   Zorn's Lemmas states: if every linear ordered subset of an ordered
-  set @{text S} has an upper bound in @{text S}, then there exists a
-  maximal element in @{text S}.  In our application, @{text S} is a
+  set \<open>S\<close> has an upper bound in \<open>S\<close>, then there exists a
+  maximal element in \<open>S\<close>.  In our application, \<open>S\<close> is a
   set of sets ordered by set inclusion. Since the union of a chain of
   sets is an upper bound for all elements of the chain, the conditions
-  of Zorn's lemma can be modified: if @{text S} is non-empty, it
-  suffices to show that for every non-empty chain @{text c} in @{text
-  S} the union of @{text c} also lies in @{text S}.
+  of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it
+  suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> also lies in \<open>S\<close>.
 \<close>
 
 theorem Zorn's_Lemma:
@@ -30,14 +29,14 @@
     show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
     proof cases
 
-      txt \<open>If @{text c} is an empty chain, then every element in
-        @{text S} is an upper bound of @{text c}.\<close>
+      txt \<open>If \<open>c\<close> is an empty chain, then every element in
+        \<open>S\<close> is an upper bound of \<open>c\<close>.\<close>
 
       assume "c = {}"
       with aS show ?thesis by fast
 
-      txt \<open>If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
-        bound of @{text c}, lying in @{text S}.\<close>
+      txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper
+        bound of \<open>c\<close>, lying in \<open>S\<close>.\<close>
 
     next
       assume "c \<noteq> {}"
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Hahn_Banach/document/root.tex
--- a/src/HOL/Hahn_Banach/document/root.tex	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Hahn_Banach/document/root.tex	Tue Nov 03 11:20:21 2015 +0100
@@ -16,7 +16,7 @@
 \pagenumbering{arabic}
 
 \title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
-\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
+\author{Gertrud Bauer}
 \maketitle
 
 \begin{abstract}
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -13,10 +13,9 @@
 
 subsection \<open>Pure backward reasoning\<close>
 
-text \<open>In order to get a first idea of how Isabelle/Isar proof
-  documents may look like, we consider the propositions @{text I},
-  @{text K}, and @{text S}.  The following (rather explicit) proofs
-  should require little extra explanations.\<close>
+text \<open>In order to get a first idea of how Isabelle/Isar proof documents may
+  look like, we consider the propositions \<open>I\<close>, \<open>K\<close>, and \<open>S\<close>. The following
+  (rather explicit) proofs should require little extra explanations.\<close>
 
 lemma I: "A \<longrightarrow> A"
 proof
@@ -51,14 +50,12 @@
   qed
 qed
 
-text \<open>Isar provides several ways to fine-tune the reasoning,
-  avoiding excessive detail.  Several abbreviated language elements
-  are available, enabling the writer to express proofs in a more
-  concise way, even without referring to any automated proof tools
-  yet.
+text \<open>Isar provides several ways to fine-tune the reasoning, avoiding
+  excessive detail. Several abbreviated language elements are available,
+  enabling the writer to express proofs in a more concise way, even without
+  referring to any automated proof tools yet.
 
-  First of all, proof by assumption may be abbreviated as a single
-  dot.\<close>
+  First of all, proof by assumption may be abbreviated as a single dot.\<close>
 
 lemma "A \<longrightarrow> A"
 proof
@@ -66,21 +63,21 @@
   show A by fact+
 qed
 
-text \<open>In fact, concluding any (sub-)proof already involves solving
-  any remaining goals by assumption\footnote{This is not a completely
-  trivial operation, as proof by assumption may involve full
-  higher-order unification.}.  Thus we may skip the rather vacuous
-  body of the above proof as well.\<close>
+text \<open>In fact, concluding any (sub-)proof already involves solving any
+  remaining goals by assumption\footnote{This is not a completely trivial
+  operation, as proof by assumption may involve full higher-order
+  unification.}. Thus we may skip the rather vacuous body of the above proof
+  as well.\<close>
 
 lemma "A \<longrightarrow> A"
 proof
 qed
 
-text \<open>Note that the \isacommand{proof} command refers to the @{text
-  rule} method (without arguments) by default.  Thus it implicitly
-  applies a single rule, as determined from the syntactic form of the
-  statements involved.  The \isacommand{by} command abbreviates any
-  proof with empty body, so the proof may be further pruned.\<close>
+text \<open>Note that the \isacommand{proof} command refers to the \<open>rule\<close> method
+  (without arguments) by default. Thus it implicitly applies a single rule,
+  as determined from the syntactic form of the statements involved. The
+  \isacommand{by} command abbreviates any proof with empty body, so the
+  proof may be further pruned.\<close>
 
 lemma "A \<longrightarrow> A"
   by rule
@@ -89,19 +86,18 @@
 
 lemma "A \<longrightarrow> A" ..
 
-text \<open>Thus we have arrived at an adequate representation of the
-  proof of a tautology that holds by a single standard
-  rule.\footnote{Apparently, the rule here is implication
-  introduction.}\<close>
+text \<open>Thus we have arrived at an adequate representation of the proof of a
+  tautology that holds by a single standard rule.\footnote{Apparently, the
+  rule here is implication introduction.}
 
-text \<open>Let us also reconsider @{text K}.  Its statement is composed
-  of iterated connectives.  Basic decomposition is by a single rule at
-  a time, which is why our first version above was by nesting two
-  proofs.
+  \<^medskip>
+  Let us also reconsider \<open>K\<close>. Its statement is composed of iterated
+  connectives. Basic decomposition is by a single rule at a time, which is
+  why our first version above was by nesting two proofs.
 
-  The @{text intro} proof method repeatedly decomposes a goal's
-  conclusion.\footnote{The dual method is @{text elim}, acting on a
-  goal's premises.}\<close>
+  The \<open>intro\<close> proof method repeatedly decomposes a goal's
+  conclusion.\footnote{The dual method is \<open>elim\<close>, acting on a goal's
+  premises.}\<close>
 
 lemma "A \<longrightarrow> B \<longrightarrow> A"
 proof (intro impI)
@@ -114,29 +110,27 @@
 lemma "A \<longrightarrow> B \<longrightarrow> A"
   by (intro impI)
 
-text \<open>Just like @{text rule}, the @{text intro} and @{text elim}
-  proof methods pick standard structural rules, in case no explicit
-  arguments are given.  While implicit rules are usually just fine for
-  single rule application, this may go too far with iteration.  Thus
-  in practice, @{text intro} and @{text elim} would be typically
-  restricted to certain structures by giving a few rules only, e.g.\
-  \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
-  and universal quantifiers.
+text \<open>Just like \<open>rule\<close>, the \<open>intro\<close> and \<open>elim\<close> proof methods pick standard
+  structural rules, in case no explicit arguments are given. While implicit
+  rules are usually just fine for single rule application, this may go too
+  far with iteration. Thus in practice, \<open>intro\<close> and \<open>elim\<close> would be
+  typically restricted to certain structures by giving a few rules only,
+  e.g.\ \isacommand{proof}~\<open>(intro impI allI)\<close> to strip implications and
+  universal quantifiers.
 
-  Such well-tuned iterated decomposition of certain structures is the
-  prime application of @{text intro} and @{text elim}.  In contrast,
-  terminal steps that solve a goal completely are usually performed by
-  actual automated proof methods (such as \isacommand{by}~@{text
-  blast}.\<close>
+  Such well-tuned iterated decomposition of certain structures is the prime
+  application of \<open>intro\<close> and \<open>elim\<close>. In contrast, terminal steps that solve
+  a goal completely are usually performed by actual automated proof methods
+  (such as \isacommand{by}~\<open>blast\<close>.\<close>
 
 
 subsection \<open>Variations of backward vs.\ forward reasoning\<close>
 
-text \<open>Certainly, any proof may be performed in backward-style only.
-  On the other hand, small steps of reasoning are often more naturally
-  expressed in forward-style.  Isar supports both backward and forward
-  reasoning as a first-class concept.  In order to demonstrate the
-  difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
+text \<open>Certainly, any proof may be performed in backward-style only. On the
+  other hand, small steps of reasoning are often more naturally expressed in
+  forward-style. Isar supports both backward and forward reasoning as a
+  first-class concept. In order to demonstrate the difference, we consider
+  several proofs of \<open>A \<and> B \<longrightarrow> B \<and> A\<close>.
 
   The first version is purely backward.\<close>
 
@@ -150,13 +144,12 @@
   qed
 qed
 
-text \<open>Above, the @{text "conjunct_1/2"} projection rules had to be
-  named explicitly, since the goals @{text B} and @{text A} did not
-  provide any structural clue.  This may be avoided using
-  \isacommand{from} to focus on the @{text "A \<and> B"} assumption as the
-  current facts, enabling the use of double-dot proofs.  Note that
-  \isacommand{from} already does forward-chaining, involving the
-  @{text conjE} rule here.\<close>
+text \<open>Above, the projection rules \<open>conjunct1\<close> / \<open>conjunct2\<close> had to be named
+  explicitly, since the goals \<open>B\<close> and \<open>A\<close> did not provide any structural
+  clue. This may be avoided using \isacommand{from} to focus on the \<open>A \<and> B\<close>
+  assumption as the current facts, enabling the use of double-dot proofs.
+  Note that \isacommand{from} already does forward-chaining, involving the
+  \<open>conjE\<close> rule here.\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -168,27 +161,26 @@
   qed
 qed
 
-text \<open>In the next version, we move the forward step one level
-  upwards.  Forward-chaining from the most recent facts is indicated
-  by the \isacommand{then} command.  Thus the proof of @{text "B \<and> A"}
-  from @{text "A \<and> B"} actually becomes an elimination, rather than an
-  introduction.  The resulting proof structure directly corresponds to
-  that of the @{text conjE} rule, including the repeated goal
-  proposition that is abbreviated as @{text ?thesis} below.\<close>
+text \<open>In the next version, we move the forward step one level upwards.
+  Forward-chaining from the most recent facts is indicated by the
+  \isacommand{then} command. Thus the proof of \<open>B \<and> A\<close> from \<open>A \<and> B\<close> actually
+  becomes an elimination, rather than an introduction. The resulting proof
+  structure directly corresponds to that of the \<open>conjE\<close> rule, including the
+  repeated goal proposition that is abbreviated as \<open>?thesis\<close> below.\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
   assume "A \<and> B"
   then show "B \<and> A"
-  proof                    -- \<open>rule @{text conjE} of @{text "A \<and> B"}\<close>
+  proof                    -- \<open>rule \<open>conjE\<close> of \<open>A \<and> B\<close>\<close>
     assume B A
-    then show ?thesis ..   -- \<open>rule @{text conjI} of @{text "B \<and> A"}\<close>
+    then show ?thesis ..   -- \<open>rule \<open>conjI\<close> of \<open>B \<and> A\<close>\<close>
   qed
 qed
 
-text \<open>In the subsequent version we flatten the structure of the main
-  body by doing forward reasoning all the time.  Only the outermost
-  decomposition step is left as backward.\<close>
+text \<open>In the subsequent version we flatten the structure of the main body by
+  doing forward reasoning all the time. Only the outermost decomposition
+  step is left as backward.\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -198,9 +190,9 @@
   from \<open>B\<close> \<open>A\<close> show "B \<and> A" ..
 qed
 
-text \<open>We can still push forward-reasoning a bit further, even at the
-  risk of getting ridiculous.  Note that we force the initial proof
-  step to do nothing here, by referring to the ``-'' proof method.\<close>
+text \<open>We can still push forward-reasoning a bit further, even at the risk of
+  getting ridiculous. Note that we force the initial proof step to do
+  nothing here, by referring to the \<open>-\<close> proof method.\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof -
@@ -210,27 +202,28 @@
     from \<open>A \<and> B\<close> have B ..
     from \<open>B\<close> \<open>A\<close> have "B \<and> A" ..
   }
-  then show ?thesis ..         -- \<open>rule @{text impI}\<close>
+  then show ?thesis ..         -- \<open>rule \<open>impI\<close>\<close>
 qed
 
-text \<open>\medskip With these examples we have shifted through a whole
-  range from purely backward to purely forward reasoning.  Apparently,
-  in the extreme ends we get slightly ill-structured proofs, which
-  also require much explicit naming of either rules (backward) or
-  local facts (forward).
+text \<open>
+  \<^medskip>
+  With these examples we have shifted through a whole range from purely
+  backward to purely forward reasoning. Apparently, in the extreme ends we
+  get slightly ill-structured proofs, which also require much explicit
+  naming of either rules (backward) or local facts (forward).
 
-  The general lesson learned here is that good proof style would
-  achieve just the \emph{right} balance of top-down backward
-  decomposition, and bottom-up forward composition.  In general, there
-  is no single best way to arrange some pieces of formal reasoning, of
-  course.  Depending on the actual applications, the intended audience
-  etc., rules (and methods) on the one hand vs.\ facts on the other
-  hand have to be emphasized in an appropriate way.  This requires the
-  proof writer to develop good taste, and some practice, of course.\<close>
+  The general lesson learned here is that good proof style would achieve
+  just the \<^emph>\<open>right\<close> balance of top-down backward decomposition, and
+  bottom-up forward composition. In general, there is no single best way to
+  arrange some pieces of formal reasoning, of course. Depending on the
+  actual applications, the intended audience etc., rules (and methods) on
+  the one hand vs.\ facts on the other hand have to be emphasized in an
+  appropriate way. This requires the proof writer to develop good taste, and
+  some practice, of course.
 
-text \<open>For our example the most appropriate way of reasoning is
-  probably the middle one, with conjunction introduction done after
-  elimination.\<close>
+  \<^medskip>
+  For our example the most appropriate way of reasoning is probably the
+  middle one, with conjunction introduction done after elimination.\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -246,50 +239,48 @@
 
 subsection \<open>A few examples from ``Introduction to Isabelle''\<close>
 
-text \<open>We rephrase some of the basic reasoning examples of
-  @{cite "isabelle-intro"}, using HOL rather than FOL.\<close>
+text \<open>We rephrase some of the basic reasoning examples of @{cite
+  "isabelle-intro"}, using HOL rather than FOL.\<close>
 
 
 subsubsection \<open>A propositional proof\<close>
 
-text \<open>We consider the proposition @{text "P \<or> P \<longrightarrow> P"}.  The proof
-  below involves forward-chaining from @{text "P \<or> P"}, followed by an
-  explicit case-analysis on the two \emph{identical} cases.\<close>
+text \<open>We consider the proposition \<open>P \<or> P \<longrightarrow> P\<close>. The proof below involves
+  forward-chaining from \<open>P \<or> P\<close>, followed by an explicit case-analysis on
+  the two \<^emph>\<open>identical\<close> cases.\<close>
 
 lemma "P \<or> P \<longrightarrow> P"
 proof
   assume "P \<or> P"
   then show P
-  proof                    -- \<open>
-    rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
-\<close>
+  proof                    -- \<open>rule \<open>disjE\<close>: \smash{$\infer{\<open>C\<close>}{\<open>A \<or> B\<close> & \infer*{\<open>C\<close>}{[\<open>A\<close>]} & \infer*{\<open>C\<close>}{[\<open>B\<close>]}}$}\<close>
     assume P show P by fact
   next
     assume P show P by fact
   qed
 qed
 
-text \<open>Case splits are \emph{not} hardwired into the Isar language as
-  a special feature.  The \isacommand{next} command used to separate
-  the cases above is just a short form of managing block structure.
+text \<open>Case splits are \<^emph>\<open>not\<close> hardwired into the Isar language as a
+  special feature. The \isacommand{next} command used to separate the cases
+  above is just a short form of managing block structure.
 
-  \medskip In general, applying proof methods may split up a goal into
-  separate ``cases'', i.e.\ new subgoals with individual local
-  assumptions.  The corresponding proof text typically mimics this by
-  establishing results in appropriate contexts, separated by blocks.
+  \<^medskip>
+  In general, applying proof methods may split up a goal into separate
+  ``cases'', i.e.\ new subgoals with individual local assumptions. The
+  corresponding proof text typically mimics this by establishing results in
+  appropriate contexts, separated by blocks.
 
   In order to avoid too much explicit parentheses, the Isar system
   implicitly opens an additional block for any new goal, the
-  \isacommand{next} statement then closes one block level, opening a
-  new one.  The resulting behavior is what one would expect from
-  separating cases, only that it is more flexible.  E.g.\ an induction
-  base case (which does not introduce local assumptions) would
-  \emph{not} require \isacommand{next} to separate the subsequent step
-  case.
+  \isacommand{next} statement then closes one block level, opening a new
+  one. The resulting behaviour is what one would expect from separating
+  cases, only that it is more flexible. E.g.\ an induction base case (which
+  does not introduce local assumptions) would \<^emph>\<open>not\<close> require
+  \isacommand{next} to separate the subsequent step case.
 
-  \medskip In our example the situation is even simpler, since the two
-  cases actually coincide.  Consequently the proof may be rephrased as
-  follows.\<close>
+  \<^medskip>
+  In our example the situation is even simpler, since the two cases actually
+  coincide. Consequently the proof may be rephrased as follows.\<close>
 
 lemma "P \<or> P \<longrightarrow> P"
 proof
@@ -316,37 +307,33 @@
 
 subsubsection \<open>A quantifier proof\<close>
 
-text \<open>To illustrate quantifier reasoning, let us prove @{text
-  "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"}.  Informally, this holds because any
-  @{text a} with @{text "P (f a)"} may be taken as a witness for the
-  second existential statement.
+text \<open>To illustrate quantifier reasoning, let us prove
+  \<open>(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)\<close>. Informally, this holds because any \<open>a\<close> with
+  \<open>P (f a)\<close> may be taken as a witness for the second existential statement.
 
-  The first proof is rather verbose, exhibiting quite a lot of
-  (redundant) detail.  It gives explicit rules, even with some
-  instantiation.  Furthermore, we encounter two new language elements:
-  the \isacommand{fix} command augments the context by some new
-  ``arbitrary, but fixed'' element; the \isacommand{is} annotation
-  binds term abbreviations by higher-order pattern matching.\<close>
+  The first proof is rather verbose, exhibiting quite a lot of (redundant)
+  detail. It gives explicit rules, even with some instantiation.
+  Furthermore, we encounter two new language elements: the \isacommand{fix}
+  command augments the context by some new ``arbitrary, but fixed'' element;
+  the \isacommand{is} annotation binds term abbreviations by higher-order
+  pattern matching.\<close>
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
   assume "\<exists>x. P (f x)"
   then show "\<exists>y. P y"
-  proof (rule exE)             -- \<open>
-    rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
-\<close>
+  proof (rule exE)             -- \<open>rule \<open>exE\<close>: \smash{$\infer{\<open>B\<close>}{\<open>\<exists>x. A(x)\<close> & \infer*{\<open>B\<close>}{[\<open>A(x)\<close>]_x}}$}\<close>
     fix a
     assume "P (f a)" (is "P ?witness")
     then show ?thesis by (rule exI [of P ?witness])
   qed
 qed
 
-text \<open>While explicit rule instantiation may occasionally improve
-  readability of certain aspects of reasoning, it is usually quite
-  redundant.  Above, the basic proof outline gives already enough
-  structural clues for the system to infer both the rules and their
-  instances (by higher-order unification).  Thus we may as well prune
-  the text as follows.\<close>
+text \<open>While explicit rule instantiation may occasionally improve readability
+  of certain aspects of reasoning, it is usually quite redundant. Above, the
+  basic proof outline gives already enough structural clues for the system
+  to infer both the rules and their instances (by higher-order unification).
+  Thus we may as well prune the text as follows.\<close>
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
@@ -359,10 +346,9 @@
   qed
 qed
 
-text \<open>Explicit @{text \<exists>}-elimination as seen above can become quite
-  cumbersome in practice.  The derived Isar language element
-  ``\isakeyword{obtain}'' provides a more handsome way to do
-  generalized existence reasoning.\<close>
+text \<open>Explicit \<open>\<exists>\<close>-elimination as seen above can become quite cumbersome in
+  practice. The derived Isar language element ``\isakeyword{obtain}''
+  provides a more handsome way to do generalized existence reasoning.\<close>
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
@@ -371,21 +357,19 @@
   then show "\<exists>y. P y" ..
 qed
 
-text \<open>Technically, \isakeyword{obtain} is similar to
-  \isakeyword{fix} and \isakeyword{assume} together with a soundness
-  proof of the elimination involved.  Thus it behaves similar to any
-  other forward proof element.  Also note that due to the nature of
-  general existence reasoning involved here, any result exported from
-  the context of an \isakeyword{obtain} statement may \emph{not} refer
-  to the parameters introduced there.\<close>
+text \<open>Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
+  \isakeyword{assume} together with a soundness proof of the elimination
+  involved. Thus it behaves similar to any other forward proof element. Also
+  note that due to the nature of general existence reasoning involved here,
+  any result exported from the context of an \isakeyword{obtain} statement
+  may \<^emph>\<open>not\<close> refer to the parameters introduced there.\<close>
 
 
 subsubsection \<open>Deriving rules in Isabelle\<close>
 
-text \<open>We derive the conjunction elimination rule from the
-  corresponding projections.  The proof is quite straight-forward,
-  since Isabelle/Isar supports non-atomic goals and assumptions fully
-  transparently.\<close>
+text \<open>We derive the conjunction elimination rule from the corresponding
+  projections. The proof is quite straight-forward, since Isabelle/Isar
+  supports non-atomic goals and assumptions fully transparently.\<close>
 
 theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
 proof -
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Cantor.thy
--- a/src/HOL/Isar_Examples/Cantor.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -12,17 +12,17 @@
   the Isabelle/HOL manual @{cite "isabelle-HOL"}.}\<close>
 
 text \<open>Cantor's Theorem states that every set has more subsets than
-  it has elements.  It has become a favorite basic example in pure
-  higher-order logic since it is so easily expressed: \[\all{f::\alpha
-  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
-  \all{x::\alpha} f \ap x \not= S\]
+  it has elements.  It has become a favourite basic example in pure
+  higher-order logic since it is so easily expressed:
+
+  @{text [display]
+  \<open>\<forall>f::\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool. \<exists>S::\<alpha> \<Rightarrow> bool. \<forall>x::\<alpha>. f x \<noteq> S\<close>}
 
-  Viewing types as sets, $\alpha \To \idt{bool}$ represents the
-  powerset of $\alpha$.  This version of the theorem states that for
-  every function from $\alpha$ to its powerset, some subset is outside
-  its range.  The Isabelle/Isar proofs below uses HOL's set theory,
-  with the type $\alpha \ap \idt{set}$ and the operator
-  $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.\<close>
+  Viewing types as sets, \<open>\<alpha> \<Rightarrow> bool\<close> represents the powerset of \<open>\<alpha>\<close>. This
+  version of the theorem states that for every function from \<open>\<alpha>\<close> to its
+  powerset, some subset is outside its range. The Isabelle/Isar proofs below
+  uses HOL's set theory, with the type \<open>\<alpha> set\<close> and the operator
+  \<open>range :: (\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> \<beta> set\<close>.\<close>
 
 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
 proof
@@ -46,20 +46,19 @@
   qed
 qed
 
-text \<open>How much creativity is required?  As it happens, Isabelle can
-  prove this theorem automatically using best-first search.
-  Depth-first search would diverge, but best-first search successfully
-  navigates through the large search space.  The context of Isabelle's
-  classical prover contains rules for the relevant constructs of HOL's
-  set theory.\<close>
+text \<open>How much creativity is required? As it happens, Isabelle can prove
+  this theorem automatically using best-first search. Depth-first search
+  would diverge, but best-first search successfully navigates through the
+  large search space. The context of Isabelle's classical prover contains
+  rules for the relevant constructs of HOL's set theory.\<close>
 
 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
   by best
 
-text \<open>While this establishes the same theorem internally, we do not
-  get any idea of how the proof actually works.  There is currently no
-  way to transform internal system-level representations of Isabelle
-  proofs back into Isar text.  Writing intelligible proof documents
-  really is a creative process, after all.\<close>
+text \<open>While this establishes the same theorem internally, we do not get any
+  idea of how the proof actually works. There is currently no way to
+  transform internal system-level representations of Isabelle proofs back
+  into Isar text. Writing intelligible proof documents really is a creative
+  process, after all.\<close>
 
 end
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Drinker.thy
--- a/src/HOL/Isar_Examples/Drinker.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Drinker.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -9,8 +9,8 @@
 begin
 
 text \<open>Here is another example of classical reasoning: the Drinker's
-  Principle says that for some person, if he is drunk, everybody else
-  is drunk!
+  Principle says that for some person, if he is drunk, everybody else is
+  drunk!
 
   We first prove a classical part of de-Morgan's law.\<close>
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Expr_Compiler.thy
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -10,17 +10,16 @@
 imports Main
 begin
 
-text \<open>This is a (rather trivial) example of program verification.
-  We model a compiler for translating expressions to stack machine
-  instructions, and prove its correctness wrt.\ some evaluation
-  semantics.\<close>
+text \<open>This is a (rather trivial) example of program verification. We model a
+  compiler for translating expressions to stack machine instructions, and
+  prove its correctness wrt.\ some evaluation semantics.\<close>
 
 
 subsection \<open>Binary operations\<close>
 
-text \<open>Binary operations are just functions over some type of values.
-  This is both for abstract syntax and semantics, i.e.\ we use a
-  ``shallow embedding'' here.\<close>
+text \<open>Binary operations are just functions over some type of values. This is
+  both for abstract syntax and semantics, i.e.\ we use a ``shallow
+  embedding'' here.\<close>
 
 type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"
 
@@ -28,16 +27,15 @@
 subsection \<open>Expressions\<close>
 
 text \<open>The language of expressions is defined as an inductive type,
-  consisting of variables, constants, and binary operations on
-  expressions.\<close>
+  consisting of variables, constants, and binary operations on expressions.\<close>
 
 datatype (dead 'adr, dead 'val) expr =
     Variable 'adr
   | Constant 'val
   | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
 
-text \<open>Evaluation (wrt.\ some environment of variable assignments) is
-  defined by primitive recursion over the structure of expressions.\<close>
+text \<open>Evaluation (wrt.\ some environment of variable assignments) is defined
+  by primitive recursion over the structure of expressions.\<close>
 
 primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
 where
@@ -48,16 +46,15 @@
 
 subsection \<open>Machine\<close>
 
-text \<open>Next we model a simple stack machine, with three
-  instructions.\<close>
+text \<open>Next we model a simple stack machine, with three instructions.\<close>
 
 datatype (dead 'adr, dead 'val) instr =
     Const 'val
   | Load 'adr
   | Apply "'val binop"
 
-text \<open>Execution of a list of stack machine instructions is easily
-  defined as follows.\<close>
+text \<open>Execution of a list of stack machine instructions is easily defined as
+  follows.\<close>
 
 primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
 where
@@ -75,8 +72,8 @@
 
 subsection \<open>Compiler\<close>
 
-text \<open>We are ready to define the compilation function of expressions
-  to lists of stack machine instructions.\<close>
+text \<open>We are ready to define the compilation function of expressions to
+  lists of stack machine instructions.\<close>
 
 primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
 where
@@ -85,9 +82,8 @@
 | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
 
 
-text \<open>The main result of this development is the correctness theorem
-  for @{text compile}.  We first establish a lemma about @{text exec}
-  and list append.\<close>
+text \<open>The main result of this development is the correctness theorem for
+  \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.\<close>
 
 lemma exec_append:
   "exec (xs @ ys) stack env =
@@ -127,11 +123,14 @@
 qed
 
 
-text \<open>\bigskip In the proofs above, the @{text simp} method does
-  quite a lot of work behind the scenes (mostly ``functional program
-  execution'').  Subsequently, the same reasoning is elaborated in
-  detail --- at most one recursive function definition is used at a
-  time.  Thus we get a better idea of what is actually going on.\<close>
+text \<open>
+  \<^bigskip>
+  In the proofs above, the \<open>simp\<close> method does quite a lot of work behind the
+  scenes (mostly ``functional program execution''). Subsequently, the same
+  reasoning is elaborated in detail --- at most one recursive function
+  definition is used at a time. Thus we get a better idea of what is
+  actually going on.
+\<close>
 
 lemma exec_append':
   "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Group.thy
--- a/src/HOL/Isar_Examples/Group.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Group.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -10,18 +10,17 @@
 
 subsection \<open>Groups and calculational reasoning\<close> 
 
-text \<open>Groups over signature $({\times} :: \alpha \To \alpha \To
-  \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$
-  are defined as an axiomatic type class as follows.  Note that the
-  parent class $\idt{times}$ is provided by the basic HOL theory.\<close>
+text \<open>Groups over signature \<open>(\<times> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, one :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close>
+  are defined as an axiomatic type class as follows. Note that the parent
+  class \<open>\<times>\<close> is provided by the basic HOL theory.\<close>
 
 class group = times + one + inverse +
   assumes group_assoc: "(x * y) * z = x * (y * z)"
     and group_left_one: "1 * x = x"
     and group_left_inverse: "inverse x * x = 1"
 
-text \<open>The group axioms only state the properties of left one and
-  inverse, the right versions may be derived as follows.\<close>
+text \<open>The group axioms only state the properties of left one and inverse,
+  the right versions may be derived as follows.\<close>
 
 theorem (in group) group_right_inverse: "x * inverse x = 1"
 proof -
@@ -44,9 +43,8 @@
   finally show ?thesis .
 qed
 
-text \<open>With \name{group-right-inverse} already available,
-  \name{group-right-one}\label{thm:group-right-one} is now established
-  much easier.\<close>
+text \<open>With \<open>group_right_inverse\<close> already available, \<open>group_right_one\<close>
+  \label{thm:group-right-one} is now established much easier.\<close>
 
 theorem (in group) group_right_one: "x * 1 = x"
 proof -
@@ -61,27 +59,27 @@
   finally show ?thesis .
 qed
 
-text \<open>\medskip The calculational proof style above follows typical
-  presentations given in any introductory course on algebra.  The
-  basic technique is to form a transitive chain of equations, which in
-  turn are established by simplifying with appropriate rules.  The
-  low-level logical details of equational reasoning are left implicit.
+text \<open>
+  \<^medskip>
+  The calculational proof style above follows typical presentations given in
+  any introductory course on algebra. The basic technique is to form a
+  transitive chain of equations, which in turn are established by
+  simplifying with appropriate rules. The low-level logical details of
+  equational reasoning are left implicit.
 
-  Note that ``$\dots$'' is just a special term variable that is bound
-  automatically to the argument\footnote{The argument of a curried
-  infix expression happens to be its right-hand side.} of the last
-  fact achieved by any local assumption or proven statement.  In
-  contrast to $\var{thesis}$, the ``$\dots$'' variable is bound
-  \emph{after} the proof is finished, though.
+  Note that ``\<open>\<dots>\<close>'' is just a special term variable that is bound
+  automatically to the argument\footnote{The argument of a curried infix
+  expression happens to be its right-hand side.} of the last fact achieved
+  by any local assumption or proven statement. In contrast to \<open>?thesis\<close>, the
+  ``\<open>\<dots>\<close>'' variable is bound \<^emph>\<open>after\<close> the proof is finished.
 
   There are only two separate Isar language elements for calculational
-  proofs: ``\isakeyword{also}'' for initial or intermediate
-  calculational steps, and ``\isakeyword{finally}'' for exhibiting the
-  result of a calculation.  These constructs are not hardwired into
-  Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
-  Expanding the \isakeyword{also} and \isakeyword{finally} derived
-  language elements, calculations may be simulated by hand as
-  demonstrated below.\<close>
+  proofs: ``\isakeyword{also}'' for initial or intermediate calculational
+  steps, and ``\isakeyword{finally}'' for exhibiting the result of a
+  calculation. These constructs are not hardwired into Isabelle/Isar, but
+  defined on top of the basic Isar/VM interpreter. Expanding the
+  \isakeyword{also} and \isakeyword{finally} derived language elements,
+  calculations may be simulated by hand as demonstrated below.\<close>
 
 theorem (in group) "x * 1 = x"
 proof -
@@ -114,51 +112,49 @@
   show ?thesis .
 qed
 
-text \<open>Note that this scheme of calculations is not restricted to
-  plain transitivity.  Rules like anti-symmetry, or even forward and
-  backward substitution work as well.  For the actual implementation
-  of \isacommand{also} and \isacommand{finally}, Isabelle/Isar
-  maintains separate context information of ``transitivity'' rules.
-  Rule selection takes place automatically by higher-order
-  unification.\<close>
+text \<open>Note that this scheme of calculations is not restricted to plain
+  transitivity. Rules like anti-symmetry, or even forward and backward
+  substitution work as well. For the actual implementation of
+  \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
+  separate context information of ``transitivity'' rules. Rule selection
+  takes place automatically by higher-order unification.\<close>
 
 
 subsection \<open>Groups as monoids\<close>
 
-text \<open>Monoids over signature $({\times} :: \alpha \To \alpha \To
-  \alpha, \idt{one} :: \alpha)$ are defined like this.\<close>
+text \<open>Monoids over signature \<open>(\<times> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, one :: \<alpha>)\<close> are defined like
+  this.\<close>
 
 class monoid = times + one +
   assumes monoid_assoc: "(x * y) * z = x * (y * z)"
     and monoid_left_one: "1 * x = x"
     and monoid_right_one: "x * 1 = x"
 
-text \<open>Groups are \emph{not} yet monoids directly from the
-  definition.  For monoids, \name{right-one} had to be included as an
-  axiom, but for groups both \name{right-one} and \name{right-inverse}
-  are derivable from the other axioms.  With \name{group-right-one}
-  derived as a theorem of group theory (see
+text \<open>Groups are \<^emph>\<open>not\<close> yet monoids directly from the definition. For
+  monoids, \<open>right_one\<close> had to be included as an axiom, but for groups both
+  \<open>right_one\<close> and \<open>right_inverse\<close> are derivable from the other axioms. With
+  \<open>group_right_one\<close> derived as a theorem of group theory (see
   page~\pageref{thm:group-right-one}), we may still instantiate
-  $\idt{group} \subseteq \idt{monoid}$ properly as follows.\<close>
+  \<open>group \<subseteq> monoid\<close> properly as follows.\<close>
 
-instance group < monoid
+instance group \<subseteq> monoid
   by intro_classes
     (rule group_assoc,
       rule group_left_one,
       rule group_right_one)
 
 text \<open>The \isacommand{instance} command actually is a version of
-  \isacommand{theorem}, setting up a goal that reflects the intended
-  class relation (or type constructor arity).  Thus any Isar proof
-  language element may be involved to establish this statement.  When
-  concluding the proof, the result is transformed into the intended
-  type signature extension behind the scenes.\<close>
+  \isacommand{theorem}, setting up a goal that reflects the intended class
+  relation (or type constructor arity). Thus any Isar proof language element
+  may be involved to establish this statement. When concluding the proof,
+  the result is transformed into the intended type signature extension
+  behind the scenes.\<close>
 
 
 subsection \<open>More theorems of group theory\<close>
 
 text \<open>The one element is already uniquely determined by preserving
-  an \emph{arbitrary} group element.\<close>
+  an \<^emph>\<open>arbitrary\<close> group element.\<close>
 
 theorem (in group) group_one_equality:
   assumes eq: "e * x = x"
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -12,11 +12,10 @@
 
 subsection \<open>Abstract syntax and semantics\<close>
 
-text \<open>The following abstract syntax and semantics of Hoare Logic
-  over \texttt{WHILE} programs closely follows the existing tradition
-  in Isabelle/HOL of formalizing the presentation given in
-  @{cite \<open>\S6\<close> "Winskel:1993"}.  See also @{file "~~/src/HOL/Hoare"} and
-  @{cite "Nipkow:1998:Winskel"}.\<close>
+text \<open>The following abstract syntax and semantics of Hoare Logic over
+  \<^verbatim>\<open>WHILE\<close> programs closely follows the existing tradition in Isabelle/HOL
+  of formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See
+  also @{file "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.\<close>
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
@@ -60,14 +59,15 @@
 
 subsection \<open>Primitive Hoare rules\<close>
 
-text \<open>From the semantics defined above, we derive the standard set
-  of primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}.
-  Usually, variant forms of these rules are applied in actual proof,
-  see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
+text \<open>From the semantics defined above, we derive the standard set of
+  primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually,
+  variant forms of these rules are applied in actual proof, see also
+  \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
 
-  \medskip The \name{basic} rule represents any kind of atomic access
-  to the state space.  This subsumes the common rules of \name{skip}
-  and \name{assign}, as formulated in \S\ref{sec:hoare-isar}.\<close>
+  \<^medskip>
+  The \<open>basic\<close> rule represents any kind of atomic access to the state space.
+  This subsumes the common rules of \<open>skip\<close> and \<open>assign\<close>, as formulated in
+  \S\ref{sec:hoare-isar}.\<close>
 
 theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
 proof
@@ -79,7 +79,7 @@
 qed
 
 text \<open>The rules for sequential commands and semantic consequences are
- established in a straight forward manner as follows.\<close>
+  established in a straight forward manner as follows.\<close>
 
 theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
 proof
@@ -105,8 +105,8 @@
 qed
 
 text \<open>The rule for conditional commands is directly reflected by the
-  corresponding semantics; in the proof we just have to look closely
-  which cases apply.\<close>
+  corresponding semantics; in the proof we just have to look closely which
+  cases apply.\<close>
 
 theorem cond:
   assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
@@ -134,12 +134,11 @@
   qed
 qed
 
-text \<open>The @{text while} rule is slightly less trivial --- it is the
-  only one based on recursion, which is expressed in the semantics by
-  a Kleene-style least fixed-point construction.  The auxiliary
-  statement below, which is by induction on the number of iterations
-  is the main point to be proven; the rest is by routine application
-  of the semantics of \texttt{WHILE}.\<close>
+text \<open>The \<open>while\<close> rule is slightly less trivial --- it is the only one based
+  on recursion, which is expressed in the semantics by a Kleene-style least
+  fixed-point construction. The auxiliary statement below, which is by
+  induction on the number of iterations is the main point to be proven; the
+  rest is by routine application of the semantics of \<^verbatim>\<open>WHILE\<close>.\<close>
 
 theorem while:
   assumes body: "\<turnstile> (P \<inter> b) c P"
@@ -167,24 +166,23 @@
 
 text \<open>We now introduce concrete syntax for describing commands (with
   embedded expressions) and assertions. The basic technique is that of
-  semantic ``quote-antiquote''.  A \emph{quotation} is a syntactic
-  entity delimited by an implicit abstraction, say over the state
-  space.  An \emph{antiquotation} is a marked expression within a
-  quotation that refers the implicit argument; a typical antiquotation
-  would select (or even update) components from the state.
+  semantic ``quote-antiquote''. A \<^emph>\<open>quotation\<close> is a syntactic entity
+  delimited by an implicit abstraction, say over the state space. An
+  \<^emph>\<open>antiquotation\<close> is a marked expression within a quotation that refers the
+  implicit argument; a typical antiquotation would select (or even update)
+  components from the state.
 
-  We will see some examples later in the concrete rules and
-  applications.\<close>
+  We will see some examples later in the concrete rules and applications.
 
-text \<open>The following specification of syntax and translations is for
-  Isabelle experts only; feel free to ignore it.
+  \<^medskip>
+  The following specification of syntax and translations is for Isabelle
+  experts only; feel free to ignore it.
 
-  While the first part is still a somewhat intelligible specification
-  of the concrete syntactic representation of our Hoare language, the
-  actual ``ML drivers'' is quite involved.  Just note that the we
-  re-use the basic quote/antiquote translations as already defined in
-  Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and
-  @{ML Syntax_Trans.quote_tr'},).\<close>
+  While the first part is still a somewhat intelligible specification of the
+  concrete syntactic representation of our Hoare language, the actual ``ML
+  drivers'' is quite involved. Just note that the we re-use the basic
+  quote/antiquote translations as already defined in Isabelle/Pure (see @{ML
+  Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},).\<close>
 
 syntax
   "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
@@ -213,10 +211,9 @@
   in [(@{syntax_const "_quote"}, K quote_tr)] end
 \<close>
 
-text \<open>As usual in Isabelle syntax translations, the part for
-  printing is more complicated --- we cannot express parts as macro
-  rules as above.  Don't look here, unless you have to do similar
-  things for yourself.\<close>
+text \<open>As usual in Isabelle syntax translations, the part for printing is
+  more complicated --- we cannot express parts as macro rules as above.
+  Don't look here, unless you have to do similar things for yourself.\<close>
 
 print_translation \<open>
   let
@@ -245,13 +242,14 @@
 
 subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close>
 
-text \<open>We are now ready to introduce a set of Hoare rules to be used
-  in single-step structured proofs in Isabelle/Isar.  We refer to the
-  concrete syntax introduce above.
+text \<open>We are now ready to introduce a set of Hoare rules to be used in
+  single-step structured proofs in Isabelle/Isar. We refer to the concrete
+  syntax introduce above.
 
-  \medskip Assertions of Hoare Logic may be manipulated in
-  calculational proofs, with the inclusion expressed in terms of sets
-  or predicates.  Reversed order is supported as well.\<close>
+  \<^medskip>
+  Assertions of Hoare Logic may be manipulated in calculational proofs, with
+  the inclusion expressed in terms of sets or predicates. Reversed order is
+  supported as well.\<close>
 
 lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
   by (unfold Valid_def) blast
@@ -278,10 +276,10 @@
   by (simp add: Valid_def)
 
 
-text \<open>Identity and basic assignments.\footnote{The $\idt{hoare}$
-  method introduced in \S\ref{sec:hoare-vcg} is able to provide proper
-  instances for any number of basic assignments, without producing
-  additional verification conditions.}\<close>
+text \<open>Identity and basic assignments.\footnote{The \<open>hoare\<close> method introduced
+  in \S\ref{sec:hoare-vcg} is able to provide proper instances for any
+  number of basic assignments, without producing additional verification
+  conditions.}\<close>
 
 lemma skip [intro?]: "\<turnstile> P SKIP P"
 proof -
@@ -293,19 +291,19 @@
   by (rule basic)
 
 text \<open>Note that above formulation of assignment corresponds to our
-  preferred way to model state spaces, using (extensible) record types
-  in HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}.  For any record field
-  $x$, Isabelle/HOL provides a functions $x$ (selector) and
-  $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder
-  appearing for the latter kind of function: due to concrete syntax
-  \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that
-  due to the external nature of HOL record fields, we could not even
-  state a general theorem relating selector and update functions (if
-  this were required here); this would only work for any particular
-  instance of record fields introduced so far.}\<close>
+  preferred way to model state spaces, using (extensible) record types in
+  HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>,
+  Isabelle/HOL provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update).
+  Above, there is only a place-holder appearing for the latter kind of
+  function: due to concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains
+  \<open>x_update\<close>.\footnote{Note that due to the external nature of HOL record
+  fields, we could not even state a general theorem relating selector and
+  update functions (if this were required here); this would only work for
+  any particular instance of record fields introduced so far.}
 
-text \<open>Sequential composition --- normalizing with associativity
-  achieves proper of chunks of code verified separately.\<close>
+  \<^medskip>
+  Sequential composition --- normalizing with associativity achieves proper
+  of chunks of code verified separately.\<close>
 
 lemmas [trans, intro?] = seq
 
@@ -344,16 +342,15 @@
 
 subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close>
 
-text \<open>We now load the \emph{original} ML file for proof scripts and
-  tactic definition for the Hoare Verification Condition Generator
-  (see @{file "~~/src/HOL/Hoare/"}).  As far as we
-  are concerned here, the result is a proof method \name{hoare}, which
-  may be applied to a Hoare Logic assertion to extract purely logical
-  verification conditions.  It is important to note that the method
-  requires \texttt{WHILE} loops to be fully annotated with invariants
-  beforehand.  Furthermore, only \emph{concrete} pieces of code are
-  handled --- the underlying tactic fails ungracefully if supplied
-  with meta-variables or parameters, for example.\<close>
+text \<open>We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic
+  definition for the Hoare Verification Condition Generator (see @{file
+  "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a
+  proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to
+  extract purely logical verification conditions. It is important to note
+  that the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with
+  invariants beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are
+  handled --- the underlying tactic fails ungracefully if supplied with
+  meta-variables or parameters, for example.\<close>
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
   by (auto simp add: Valid_def)
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -6,9 +6,9 @@
 
 subsection \<open>State spaces\<close>
 
-text \<open>First of all we provide a store of program variables that
-  occur in any of the programs considered later.  Slightly unexpected
-  things may happen when attempting to work with undeclared variables.\<close>
+text \<open>First of all we provide a store of program variables that occur in any
+  of the programs considered later. Slightly unexpected things may happen
+  when attempting to work with undeclared variables.\<close>
 
 record vars =
   I :: nat
@@ -16,29 +16,28 @@
   N :: nat
   S :: nat
 
-text \<open>While all of our variables happen to have the same type,
-  nothing would prevent us from working with many-sorted programs as
-  well, or even polymorphic ones.  Also note that Isabelle/HOL's
-  extensible record types even provides simple means to extend the
-  state space later.\<close>
+text \<open>While all of our variables happen to have the same type, nothing would
+  prevent us from working with many-sorted programs as well, or even
+  polymorphic ones. Also note that Isabelle/HOL's extensible record types
+  even provides simple means to extend the state space later.\<close>
 
 
 subsection \<open>Basic examples\<close>
 
-text \<open>We look at few trivialities involving assignment and
-  sequential composition, in order to get an idea of how to work with
-  our formulation of Hoare Logic.\<close>
+text \<open>We look at few trivialities involving assignment and sequential
+  composition, in order to get an idea of how to work with our formulation
+  of Hoare Logic.\<close>
 
-text \<open>Using the basic @{text assign} rule directly is a bit
+text \<open>Using the basic \<open>assign\<close> rule directly is a bit
   cumbersome.\<close>
 
 lemma "\<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
   by (rule assign)
 
-text \<open>Certainly we want the state modification already done, e.g.\
-  by simplification.  The \name{hoare} method performs the basic state
-  update for us; we may apply the Simplifier afterwards to achieve
-  ``obvious'' consequences as well.\<close>
+text \<open>Certainly we want the state modification already done, e.g.\ by
+  simplification. The \<open>hoare\<close> method performs the basic state update for us;
+  we may apply the Simplifier afterwards to achieve ``obvious'' consequences
+  as well.\<close>
 
 lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>"
   by hoare
@@ -67,8 +66,8 @@
       \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
   by hoare simp
 
-text \<open>It is important to note that statements like the following one
-  can only be proven for each individual program variable.  Due to the
+text \<open>It is important to note that statements like the following one can
+  only be proven for each individual program variable. Due to the
   extra-logical nature of record fields, we cannot formulate a theorem
   relating record selectors and updates schematically.\<close>
 
@@ -84,9 +83,9 @@
   oops
 
 
-text \<open>In the following assignments we make use of the consequence
-  rule in order to achieve the intended precondition.  Certainly, the
-  \name{hoare} method is able to handle this case, too.\<close>
+text \<open>In the following assignments we make use of the consequence rule in
+  order to achieve the intended precondition. Certainly, the \<open>hoare\<close> method
+  is able to handle this case, too.\<close>
 
 lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
 proof -
@@ -114,10 +113,10 @@
 
 subsection \<open>Multiplication by addition\<close>
 
-text \<open>We now do some basic examples of actual \texttt{WHILE}
-  programs.  This one is a loop for calculating the product of two
-  natural numbers, by iterated addition.  We first give detailed
-  structured proof based on single-step Hoare rules.\<close>
+text \<open>We now do some basic examples of actual \<^verbatim>\<open>WHILE\<close> programs. This one is
+  a loop for calculating the product of two natural numbers, by iterated
+  addition. We first give detailed structured proof based on single-step
+  Hoare rules.\<close>
 
 lemma
   "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@@ -141,10 +140,10 @@
   finally show ?thesis .
 qed
 
-text \<open>The subsequent version of the proof applies the @{text hoare}
-  method to reduce the Hoare statement to a purely logical problem
-  that can be solved fully automatically.  Note that we have to
-  specify the \texttt{WHILE} loop invariant in the original statement.\<close>
+text \<open>The subsequent version of the proof applies the \<open>hoare\<close> method to
+  reduce the Hoare statement to a purely logical problem that can be solved
+  fully automatically. Note that we have to specify the \<^verbatim>\<open>WHILE\<close> loop
+  invariant in the original statement.\<close>
 
 lemma
   "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@@ -157,15 +156,15 @@
 
 subsection \<open>Summing natural numbers\<close>
 
-text \<open>We verify an imperative program to sum natural numbers up to a
-  given limit.  First some functional definition for proper
-  specification of the problem.\<close>
+text \<open>We verify an imperative program to sum natural numbers up to a given
+  limit. First some functional definition for proper specification of the
+  problem.
 
-text \<open>The following proof is quite explicit in the individual steps
-  taken, with the \name{hoare} method only applied locally to take
-  care of assignment and sequential composition.  Note that we express
-  intermediate proof obligation in pure logic, without referring to
-  the state space.\<close>
+  \<^medskip>
+  The following proof is quite explicit in the individual steps taken, with
+  the \<open>hoare\<close> method only applied locally to take care of assignment and
+  sequential composition. Note that we express intermediate proof obligation
+  in pure logic, without referring to the state space.\<close>
 
 theorem
   "\<turnstile> \<lbrace>True\<rbrace>
@@ -203,9 +202,8 @@
   finally show ?thesis .
 qed
 
-text \<open>The next version uses the @{text hoare} method, while still
-  explaining the resulting proof obligations in an abstract,
-  structured manner.\<close>
+text \<open>The next version uses the \<open>hoare\<close> method, while still explaining the
+  resulting proof obligations in an abstract, structured manner.\<close>
 
 theorem
   "\<turnstile> \<lbrace>True\<rbrace>
@@ -230,8 +228,8 @@
   qed
 qed
 
-text \<open>Certainly, this proof may be done fully automatic as well,
-  provided that the invariant is given beforehand.\<close>
+text \<open>Certainly, this proof may be done fully automatic as well, provided
+  that the invariant is given beforehand.\<close>
 
 theorem
   "\<turnstile> \<lbrace>True\<rbrace>
@@ -248,8 +246,8 @@
 
 subsection \<open>Time\<close>
 
-text \<open>A simple embedding of time in Hoare logic: function @{text
-  timeit} inserts an extra variable to keep track of the elapsed time.\<close>
+text \<open>A simple embedding of time in Hoare logic: function \<open>timeit\<close> inserts
+  an extra variable to keep track of the elapsed time.\<close>
 
 record tstate = time :: nat
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Knaster_Tarski.thy
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -14,30 +14,27 @@
 subsection \<open>Prose version\<close>
 
 text \<open>According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"},
-  the Knaster-Tarski fixpoint theorem is as
-  follows.\footnote{We have dualized the argument, and tuned the
-  notation a little bit.}
-
-  \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let @{text L} be a
-  complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
-  Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}.
+  the Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
+  dualized the argument, and tuned the notation a little bit.}
 
-  \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a =
-  \<Sqinter>H"}.  For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text
-  "f(a) \<le> f(x) \<le> x"}.  Thus @{text "f(a)"} is a lower bound of @{text
-  H}, whence @{text "f(a) \<le> a"}.  We now use this inequality to prove
-  the reverse one (!) and thereby complete the proof that @{text a} is
-  a fixpoint.  Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
-  f(a)"}.  This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.\<close>
+  \<^bold>\<open>The Knaster-Tarski Fixpoint Theorem.\<close> Let \<open>L\<close> be a complete lattice and
+  \<open>f: L \<rightarrow> L\<close> an order-preserving map. Then \<open>\<Sqinter>{x \<in> L | f(x) \<le> x}\<close> is a
+  fixpoint of \<open>f\<close>.
+
+  \<^bold>\<open>Proof.\<close> Let \<open>H = {x \<in> L | f(x) \<le> x}\<close> and \<open>a = \<Sqinter>H\<close>. For all \<open>x \<in> H\<close> we
+  have \<open>a \<le> x\<close>, so \<open>f(a) \<le> f(x) \<le> x\<close>. Thus \<open>f(a)\<close> is a lower bound of \<open>H\<close>,
+  whence \<open>f(a) \<le> a\<close>. We now use this inequality to prove the reverse one (!)
+  and thereby complete the proof that \<open>a\<close> is a fixpoint. Since \<open>f\<close> is
+  order-preserving, \<open>f(f(a)) \<le> f(a)\<close>. This says \<open>f(a) \<in> H\<close>, so \<open>a \<le> f(a)\<close>.\<close>
 
 
 subsection \<open>Formal versions\<close>
 
-text \<open>The Isar proof below closely follows the original
-  presentation.  Virtually all of the prose narration has been
-  rephrased in terms of formal Isar language elements.  Just as many
-  textbook-style proofs, there is a strong bias towards forward proof,
-  and several bends in the course of reasoning.\<close>
+text \<open>The Isar proof below closely follows the original presentation.
+  Virtually all of the prose narration has been rephrased in terms of formal
+  Isar language elements. Just as many textbook-style proofs, there is a
+  strong bias towards forward proof, and several bends in the course of
+  reasoning.\<close>
 
 theorem Knaster_Tarski:
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
@@ -67,15 +64,15 @@
   qed
 qed
 
-text \<open>Above we have used several advanced Isar language elements,
-  such as explicit block structure and weak assumptions.  Thus we have
-  mimicked the particular way of reasoning of the original text.
+text \<open>Above we have used several advanced Isar language elements, such as
+  explicit block structure and weak assumptions. Thus we have mimicked the
+  particular way of reasoning of the original text.
 
-  In the subsequent version the order of reasoning is changed to
-  achieve structured top-down decomposition of the problem at the
-  outer level, while only the inner steps of reasoning are done in a
-  forward manner.  We are certainly more at ease here, requiring only
-  the most basic features of the Isar language.\<close>
+  In the subsequent version the order of reasoning is changed to achieve
+  structured top-down decomposition of the problem at the outer level, while
+  only the inner steps of reasoning are done in a forward manner. We are
+  certainly more at ease here, requiring only the most basic features of the
+  Isar language.\<close>
 
 theorem Knaster_Tarski':
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -9,8 +9,8 @@
 imports Main
 begin
 
-text \<open>The Mutilated Checker Board Problem, formalized inductively.
-  See @{cite "paulson-mutilated-board"} for the original tactic script version.\<close>
+text \<open>The Mutilated Checker Board Problem, formalized inductively. See @{cite
+  "paulson-mutilated-board"} for the original tactic script version.\<close>
 
 subsection \<open>Tilings\<close>
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Nested_Datatype.thy
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -20,7 +20,7 @@
 
 lemmas subst_simps = subst_term.simps subst_term_list.simps
 
-text \<open>\medskip A simple lemma about composition of substitutions.\<close>
+text \<open>\<^medskip> A simple lemma about composition of substitutions.\<close>
 
 lemma
   "subst_term (subst_term f1 \<circ> f2) t =
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Peirce.thy
--- a/src/HOL/Isar_Examples/Peirce.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Peirce.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -8,16 +8,15 @@
 imports Main
 begin
 
-text \<open>We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.
-  This is an inherently non-intuitionistic statement, so its proof
-  will certainly involve some form of classical contradiction.
+text \<open>We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently
+  non-intuitionistic statement, so its proof will certainly involve some
+  form of classical contradiction.
 
-  The first proof is again a well-balanced combination of plain
-  backward and forward reasoning.  The actual classical step is where
-  the negated goal may be introduced as additional assumption.  This
-  eventually leads to a contradiction.\footnote{The rule involved
-  there is negation elimination; it holds in intuitionistic logic as
-  well.}\<close>
+  The first proof is again a well-balanced combination of plain backward and
+  forward reasoning. The actual classical step is where the negated goal may
+  be introduced as additional assumption. This eventually leads to a
+  contradiction.\footnote{The rule involved there is negation elimination;
+  it holds in intuitionistic logic as well.}\<close>
 
 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
@@ -34,19 +33,17 @@
   qed
 qed
 
-text \<open>In the subsequent version the reasoning is rearranged by means
-  of ``weak assumptions'' (as introduced by \isacommand{presume}).
-  Before assuming the negated goal $\neg A$, its intended consequence
-  $A \impl B$ is put into place in order to solve the main problem.
-  Nevertheless, we do not get anything for free, but have to establish
-  $A \impl B$ later on.  The overall effect is that of a logical
-  \emph{cut}.
+text \<open>In the subsequent version the reasoning is rearranged by means of
+  ``weak assumptions'' (as introduced by \isacommand{presume}). Before
+  assuming the negated goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put
+  into place in order to solve the main problem. Nevertheless, we do not get
+  anything for free, but have to establish \<open>A \<longrightarrow> B\<close> later on. The overall
+  effect is that of a logical \<^emph>\<open>cut\<close>.
 
-  Technically speaking, whenever some goal is solved by
-  \isacommand{show} in the context of weak assumptions then the latter
-  give rise to new subgoals, which may be established separately.  In
-  contrast, strong assumptions (as introduced by \isacommand{assume})
-  are solved immediately.\<close>
+  Technically speaking, whenever some goal is solved by \isacommand{show} in
+  the context of weak assumptions then the latter give rise to new subgoals,
+  which may be established separately. In contrast, strong assumptions (as
+  introduced by \isacommand{assume}) are solved immediately.\<close>
 
 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
@@ -65,21 +62,20 @@
   qed
 qed
 
-text \<open>Note that the goals stemming from weak assumptions may be even
-  left until qed time, where they get eventually solved ``by
-  assumption'' as well.  In that case there is really no fundamental
-  difference between the two kinds of assumptions, apart from the
-  order of reducing the individual parts of the proof configuration.
+text \<open>Note that the goals stemming from weak assumptions may be even left
+  until qed time, where they get eventually solved ``by assumption'' as
+  well. In that case there is really no fundamental difference between the
+  two kinds of assumptions, apart from the order of reducing the individual
+  parts of the proof configuration.
 
-  Nevertheless, the ``strong'' mode of plain assumptions is quite
-  important in practice to achieve robustness of proof text
-  interpretation.  By forcing both the conclusion \emph{and} the
-  assumptions to unify with the pending goal to be solved, goal
-  selection becomes quite deterministic.  For example, decomposition
-  with rules of the ``case-analysis'' type usually gives rise to
-  several goals that only differ in there local contexts.  With strong
-  assumptions these may be still solved in any order in a predictable
-  way, while weak ones would quickly lead to great confusion,
-  eventually demanding even some backtracking.\<close>
+  Nevertheless, the ``strong'' mode of plain assumptions is quite important
+  in practice to achieve robustness of proof text interpretation. By forcing
+  both the conclusion \<^emph>\<open>and\<close> the assumptions to unify with the pending goal
+  to be solved, goal selection becomes quite deterministic. For example,
+  decomposition with rules of the ``case-analysis'' type usually gives rise
+  to several goals that only differ in there local contexts. With strong
+  assumptions these may be still solved in any order in a predictable way,
+  while weak ones would quickly lead to great confusion, eventually
+  demanding even some backtracking.\<close>
 
 end
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Puzzle.thy
--- a/src/HOL/Isar_Examples/Puzzle.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -8,9 +8,8 @@
   Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
   script by Tobias Nipkow.}\<close>
 
-text \<open>\textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$
-  such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
-  Demonstrate that $f$ is the identity.\<close>
+text \<open>\<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that
+  \<open>f (f n) < f (Suc n)\<close> for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.\<close>
 
 theorem
   assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/Summation.thy
--- a/src/HOL/Isar_Examples/Summation.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -9,16 +9,16 @@
 begin
 
 text \<open>Subsequently, we prove some summation laws of natural numbers
-  (including odds, squares, and cubes).  These examples demonstrate
-  how plain natural deduction (including induction) may be combined
-  with calculational proof.\<close>
+  (including odds, squares, and cubes). These examples demonstrate how plain
+  natural deduction (including induction) may be combined with calculational
+  proof.\<close>
 
 
 subsection \<open>Summation laws\<close>
 
-text \<open>The sum of natural numbers $0 + \cdots + n$ equals $n \times
-  (n + 1)/2$.  Avoiding formal reasoning about division we prove this
-  equation multiplied by $2$.\<close>
+text \<open>The sum of natural numbers \<open>0 + \<cdots> + n\<close> equals \<open>n \<times> (n + 1)/2\<close>.
+  Avoiding formal reasoning about division we prove this equation multiplied
+  by \<open>2\<close>.\<close>
 
 theorem sum_of_naturals:
   "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
@@ -35,47 +35,39 @@
     by simp
 qed
 
-text \<open>The above proof is a typical instance of mathematical
-  induction.  The main statement is viewed as some $\var{P} \ap n$
-  that is split by the induction method into base case $\var{P} \ap
-  0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap
-  n)$ for arbitrary $n$.
+text \<open>The above proof is a typical instance of mathematical induction. The
+  main statement is viewed as some \<open>?P n\<close> that is split by the induction
+  method into base case \<open>?P 0\<close>, and step case \<open>?P n \<Longrightarrow> ?P (Suc n)\<close> for
+  arbitrary \<open>n\<close>.
 
-  The step case is established by a short calculation in forward
-  manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
-  the thesis, the final result is achieved by transformations
-  involving basic arithmetic reasoning (using the Simplifier).  The
-  main point is where the induction hypothesis $\var{S} \ap n = n
-  \times (n + 1)$ is introduced in order to replace a certain subterm.
-  So the ``transitivity'' rule involved here is actual
-  \emph{substitution}.  Also note how the occurrence of ``\dots'' in
-  the subsequent step documents the position where the right-hand side
-  of the hypothesis got filled in.
+  The step case is established by a short calculation in forward manner.
+  Starting from the left-hand side \<open>?S (n + 1)\<close> of the thesis, the final
+  result is achieved by transformations involving basic arithmetic reasoning
+  (using the Simplifier). The main point is where the induction hypothesis
+  \<open>?S n = n \<times> (n + 1)\<close> is introduced in order to replace a certain subterm.
+  So the ``transitivity'' rule involved here is actual \<^emph>\<open>substitution\<close>. Also
+  note how the occurrence of ``\dots'' in the subsequent step documents the
+  position where the right-hand side of the hypothesis got filled in.
 
-  \medskip A further notable point here is integration of calculations
-  with plain natural deduction.  This works so well in Isar for two
-  reasons.
-  \begin{enumerate}
-
-  \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
-  calculational chains may be just anything.  There is nothing special
-  about \isakeyword{have}, so the natural deduction element
-  \isakeyword{assume} works just as well.
+  \<^medskip>
+  A further notable point here is integration of calculations with plain
+  natural deduction. This works so well in Isar for two reasons.
 
-  \item There are two \emph{separate} primitives for building natural
-  deduction contexts: \isakeyword{fix}~$x$ and
-  \isakeyword{assume}~$A$.  Thus it is possible to start reasoning
-  with some new ``arbitrary, but fixed'' elements before bringing in
-  the actual assumption.  In contrast, natural deduction is
-  occasionally formalized with basic context elements of the form
-  $x:A$ instead.
+    \<^enum> Facts involved in \isakeyword{also}~/ \isakeyword{finally}
+    calculational chains may be just anything. There is nothing special
+    about \isakeyword{have}, so the natural deduction element
+    \isakeyword{assume} works just as well.
+  
+    \<^enum> There are two \<^emph>\<open>separate\<close> primitives for building natural deduction
+    contexts: \isakeyword{fix}~\<open>x\<close> and \isakeyword{assume}~\<open>A\<close>. Thus it is
+    possible to start reasoning with some new ``arbitrary, but fixed''
+    elements before bringing in the actual assumption. In contrast, natural
+    deduction is occasionally formalized with basic context elements of the
+    form \<open>x:A\<close> instead.
 
-  \end{enumerate}
-\<close>
-
-text \<open>\medskip We derive further summation laws for odds, squares,
-  and cubes as follows.  The basic technique of induction plus
-  calculation is the same as before.\<close>
+  \<^medskip>
+  We derive further summation laws for odds, squares, and cubes as follows.
+  The basic technique of induction plus calculation is the same as before.\<close>
 
 theorem sum_of_odds:
   "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
@@ -93,9 +85,8 @@
     by simp
 qed
 
-text \<open>Subsequently we require some additional tweaking of Isabelle
-  built-in arithmetic simplifications, such as bringing in
-  distributivity by hand.\<close>
+text \<open>Subsequently we require some additional tweaking of Isabelle built-in
+  arithmetic simplifications, such as bringing in distributivity by hand.\<close>
 
 lemmas distrib = add_mult_distrib add_mult_distrib2
 
@@ -134,15 +125,13 @@
 
 text \<open>Note that in contrast to older traditions of tactical proof
   scripts, the structured proof applies induction on the original,
-  unsimplified statement.  This allows to state the induction cases
-  robustly and conveniently.  Simplification (or other automated)
-  methods are then applied in terminal position to solve certain
-  sub-problems completely.
+  unsimplified statement. This allows to state the induction cases robustly
+  and conveniently. Simplification (or other automated) methods are then
+  applied in terminal position to solve certain sub-problems completely.
 
-  As a general rule of good proof style, automatic methods such as
-  $\idt{simp}$ or $\idt{auto}$ should normally be never used as
-  initial proof methods with a nested sub-proof to address the
-  automatically produced situation, but only as terminal ones to solve
-  sub-problems.\<close>
+  As a general rule of good proof style, automatic methods such as \<open>simp\<close> or
+  \<open>auto\<close> should normally be never used as initial proof methods with a
+  nested sub-proof to address the automatically produced situation, but only
+  as terminal ones to solve sub-problems.\<close>
 
 end
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Tue Nov 03 11:20:21 2015 +0100
@@ -1,11 +1,22 @@
-\input{style}
+\documentclass[11pt,a4paper]{article}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
+\isabellestyle{it}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+\renewcommand{\isacommand}[1]
+{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
+  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
+
+\newcommand{\DUMMYPROOF}{{\langle\mathit{proof}\rangle}}
+\newcommand{\dummyproof}{$\DUMMYPROOF$}
 
 \hyphenation{Isabelle}
 
 \begin{document}
 
 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
-\author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex]
+\author{Markus Wenzel \\[2ex]
   With contributions by Gertrud Bauer and Tobias Nipkow}
 \maketitle
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Isar_Examples/document/style.tex
--- a/src/HOL/Isar_Examples/document/style.tex	Mon Nov 02 16:17:09 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
-\isabellestyle{it}
-\usepackage{pdfsetup}\urlstyle{rm}
-
-\renewcommand{\isacommand}[1]
-{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
-  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
-
-\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
-\newcommand{\dummyproof}{$\DUMMYPROOF$}
-
-\newcommand{\name}[1]{\textsl{#1}}
-
-\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
-\newcommand{\var}[1]{{?\!\idt{#1}}}
-\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
-\newcommand{\dsh}{\dshsym}
-
-\newcommand{\To}{\to}
-\newcommand{\dt}{{\mathpunct.}}
-\newcommand{\ap}{\mathbin{\!}}
-\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\all}[1]{\forall #1\dt\;}
-\newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\impl}{\to}
-\newcommand{\conj}{\land}
-\newcommand{\disj}{\lor}
-\newcommand{\Impl}{\Longrightarrow}
-
-\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy	Tue Nov 03 11:20:21 2015 +0100
@@ -1,4 +1,4 @@
-(* Author: Steven Obua, TU Muenchen *)
+(*  Author:     Steven Obua, TU Muenchen *)
 
 section \<open>Various algebraic structures combined with a lattice\<close>
 
@@ -224,7 +224,7 @@
   proof -
     from that have a: "inf (a + a) 0 = 0"
       by (simp add: inf_commute inf_absorb1)
-    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
+    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l = _")
       by (simp add: add_sup_inf_distribs inf_aci)
     then have "?l = 0 + inf a 0"
       by (simp add: a, simp add: inf_commute)
@@ -619,4 +619,3 @@
 qed
 
 end
-
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/ROOT	Tue Nov 03 11:20:21 2015 +0100
@@ -647,7 +647,6 @@
   document_files
     "root.bib"
     "root.tex"
-    "style.tex"
 
 session "HOL-Eisbach" in Eisbach = HOL +
   description {*
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Nov 03 11:20:21 2015 +0100
@@ -397,15 +397,20 @@
     val dfg = (case format of DFG _ => true | _ => false)
     fun str _ (AType ((s, _), [])) =
         if dfg andalso s = tptp_individual_type then dfg_individual_type else s
-      | str _ (AType ((s, _), tys)) =
-        let val ss = tys |> map (str false) in
-          if s = tptp_product_type then
-            ss |> space_implode
-                      (if dfg then ", " else " " ^ tptp_product_type ^ " ")
-               |> (not dfg andalso length ss > 1) ? parens
-          else
-            tptp_string_of_app format s ss
-        end
+      | str rhs (AType ((s, _), tys)) =
+        if s = tptp_fun_type then
+          let val [ty1, ty2] = tys in
+            str rhs (AFun (ty1, ty2))
+          end
+        else
+          let val ss = tys |> map (str false) in
+            if s = tptp_product_type then
+              ss |> space_implode
+                        (if dfg then ", " else " " ^ tptp_product_type ^ " ")
+                 |> (not dfg andalso length ss > 1) ? parens
+            else
+              tptp_string_of_app format s ss
+          end
       | str rhs (AFun (ty1, ty2)) =
         (str false ty1 |> dfg ? parens) ^ " " ^
         (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Nov 03 11:20:21 2015 +0100
@@ -105,14 +105,13 @@
   val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
   val transfer_gfp_sugar_thms: theory -> gfp_sugar_thms -> gfp_sugar_thms
 
-  val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
-     typ list -> typ list -> int list -> int list list -> term list -> Proof.context ->
-     (term list
-      * (typ list list * typ list list list list * term list list * term list list list list) option
-      * (string * term list * term list list
-         * (((term list list * term list list * term list list list list * term list list list list)
-             * term list list list) * typ list)) option)
-     * Proof.context
+  val mk_co_recs_prelims: Proof.context -> BNF_Util.fp_kind -> typ list list list -> typ list ->
+     typ list -> typ list -> typ list -> int list -> int list list -> term list ->
+     term list
+     * (typ list list * typ list list list list * term list list * term list list list list) option
+     * (string * term list * term list list
+        * (((term list list * term list list * term list list list list * term list list list list)
+            * term list list list) * typ list)) option
   val repair_nullary_single_ctr: typ list list -> typ list list
   val mk_corec_p_pred_types: typ list -> int list -> typ list list
   val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
@@ -1176,7 +1175,7 @@
   | unzip_recT _ (Type (@{type_name prod}, Ts as [_, TFree _])) = Ts
   | unzip_recT _ T = [T];
 
-fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
+fun mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts =
   let
     val Css = map2 replicate ns Cs;
     val x_Tssss =
@@ -1188,11 +1187,11 @@
     val x_Tsss' = map (map flat_rec_arg_args) x_Tssss;
     val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css;
 
-    val ((fss, xssss), lthy) = lthy
+    val ((fss, xssss), _) = ctxt
       |> mk_Freess "f" f_Tss
       ||>> mk_Freessss "x" x_Tssss;
   in
-    ((f_Tss, x_Tssss, fss, xssss), lthy)
+    (f_Tss, x_Tssss, fss, xssss)
   end;
 
 fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
@@ -1222,14 +1221,14 @@
    mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
      (binder_fun_types (fastype_of dtor_corec)));
 
-fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy =
+fun mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts =
   let
     val p_Tss = mk_corec_p_pred_types Cs ns;
 
     val (q_Tssss, g_Tsss, g_Tssss, corec_types) =
       mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts;
 
-    val (((((Free (x, _), cs), pss), qssss), gssss), lthy) = lthy
+    val (((((Free (x, _), cs), pss), qssss), gssss), _) = ctxt
       |> yield_singleton (mk_Frees "x") dummyT
       ||>> mk_Frees "a" Cs
       ||>> mk_Freess "p" p_Tss
@@ -1238,7 +1237,7 @@
 
     val cpss = map2 (map o rapp) cs pss;
 
-    fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd);
+    fun build_sum_inj mk_inj = build_map ctxt [] (uncurry mk_inj o dest_sumT o snd);
 
     fun build_dtor_corec_arg _ [] [cg] = cg
       | build_dtor_corec_arg T [cq] [cg, cg'] =
@@ -1250,25 +1249,25 @@
     val cgssss = map2 (map o map o map o rapp) cs gssss;
     val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss;
   in
-    ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy)
+    (x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types))
   end;
 
-fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
+fun mk_co_recs_prelims ctxt fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 =
   let
-    val thy = Proof_Context.theory_of lthy;
+    val thy = Proof_Context.theory_of ctxt;
 
     val (xtor_co_rec_fun_Ts, xtor_co_recs) =
       mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd);
 
-    val ((recs_args_types, corecs_args_types), lthy') =
+    val (recs_args_types, corecs_args_types) =
       if fp = Least_FP then
-        mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
-        |>> (rpair NONE o SOME)
+        mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts
+        |> (rpair NONE o SOME)
       else
-        mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
-        |>> (pair NONE o SOME);
+        mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts
+        |> (pair NONE o SOME);
   in
-    ((xtor_co_recs, recs_args_types, corecs_args_types), lthy')
+    (xtor_co_recs, recs_args_types, corecs_args_types)
   end;
 
 fun mk_preds_getterss_join c cps absT abs cqgss =
@@ -2175,8 +2174,9 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
-      mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
+    val (xtor_co_recs, recs_args_types, corecs_args_types) =
+      mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
+    val lthy' = lthy;
 
     fun define_ctrs_dtrs_for_type fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
         ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Nov 03 11:20:21 2015 +0100
@@ -255,8 +255,8 @@
         val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
         val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
 
-        val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
-          mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
+        val (xtor_co_recs, recs_args_types, corecs_args_types) =
+          mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
 
         fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;
 
diff -r 980dd46a03fb -r 933eb9e6a1cc src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Nov 03 11:20:21 2015 +0100
@@ -462,16 +462,22 @@
           else
             sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms raw_sel_bindingss;
 
+    val add_bindings =
+      Variable.add_fixes (distinct (op =) (filter Symbol_Pos.is_identifier
+        (map Binding.name_of (disc_bindings @ flat sel_bindingss))))
+      #> snd;
+
     val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val ((((((((exh_y, xss), yss), fs), gs), u), w), (p, p'))) =
+    val ((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))) =
       no_defs_lthy
-      |> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *)
+      |> add_bindings
+      |> yield_singleton (mk_Frees fc_b_name) fcT
+      ||>> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *)
       ||>> mk_Freess "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
-      ||>> yield_singleton (mk_Frees fc_b_name) fcT
       ||>> yield_singleton (mk_Frees "z") B
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT
       |> fst;
@@ -673,13 +679,14 @@
 
     fun after_qed ([exhaust_thm] :: thmss) lthy =
       let
-        val ((((((((xss, xss'), fs), gs), h), (u, u')), v), p), _) =
+        val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) =
           lthy
-          |> mk_Freess' "x" ctr_Tss
+          |> add_bindings
+          |> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT
+          ||>> mk_Freess' "x" ctr_Tss
           ||>> mk_Frees "f" case_Ts
           ||>> mk_Frees "g" case_Ts
           ||>> yield_singleton (mk_Frees "h") (B --> C)
-          ||>> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT
           ||>> yield_singleton (mk_Frees (fc_b_name ^ "'")) fcT
           ||>> yield_singleton (mk_Frees "P") HOLogic.boolT;
 
@@ -687,18 +694,18 @@
         val xgs = map2 (curry Term.list_comb) gs xss;
 
         val fcase = Term.list_comb (casex, fs);
-    
+
         val ufcase = fcase $ u;
         val vfcase = fcase $ v;
-    
+
         val eta_fcase = Term.list_comb (casex, eta_fs);
         val eta_gcase = Term.list_comb (casex, eta_gs);
-    
+
         val eta_ufcase = eta_fcase $ u;
         val eta_vgcase = eta_gcase $ v;
 
         fun mk_uu_eq () = HOLogic.mk_eq (u, u);
-    
+
         val uv_eq = mk_Trueprop_eq (u, v);
 
         val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
diff -r 980dd46a03fb -r 933eb9e6a1cc src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Nov 03 11:20:21 2015 +0100
@@ -36,7 +36,7 @@
   val language_prop: bool -> T
   val language_ML: bool -> T
   val language_SML: bool -> T
-  val language_document: bool -> T
+  val language_document: {symbols: bool, delimited: bool} -> T
   val language_antiquotation: T
   val language_text: bool -> T
   val language_rail: T
@@ -310,7 +310,8 @@
 val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
 val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
-val language_document = language' {name = "document", symbols = false, antiquotes = true};
+fun language_document {symbols, delimited} =
+  language' {name = "document", symbols = symbols, antiquotes = true} delimited;
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
diff -r 980dd46a03fb -r 933eb9e6a1cc src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Tue Nov 03 11:20:21 2015 +0100
@@ -16,6 +16,26 @@
     val RUNNING = Value("running")
     val FINISHED = Value("finished")
   }
+
+  object State
+  {
+    val empty: State = State()
+
+    def make(command: Command, query: List[String]): State =
+      State(instance = Document_ID.make().toString,
+        location = Some(command),
+        query = query,
+        status = Status.WAITING)
+  }
+
+  sealed case class State(
+    instance: String = Document_ID.none.toString,
+    location: Option[Command] = None,
+    query: List[String] = Nil,
+    update_pending: Boolean = false,
+    output: List[XML.Tree] = Nil,
+    status: Status.Value = Status.FINISHED,
+    exec_id: Document_ID.Exec = Document_ID.none)
 }
 
 class Query_Operation[Editor_Context](
@@ -26,37 +46,19 @@
   consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
 {
   private val print_function = operation_name + "_query"
-  private val instance = Document_ID.make().toString
 
 
   /* implicit state -- owned by GUI thread */
 
-  @volatile private var current_location: Option[Command] = None
-  @volatile private var current_query: List[String] = Nil
-  @volatile private var current_update_pending = false
-  @volatile private var current_output: List[XML.Tree] = Nil
-  @volatile private var current_status = Query_Operation.Status.FINISHED
-  @volatile private var current_exec_id = Document_ID.none
-
-  def get_location: Option[Command] = current_location
+  private val current_state = Synchronized(Query_Operation.State.empty)
 
-  private def reset_state()
-  {
-    current_location = None
-    current_query = Nil
-    current_update_pending = false
-    current_output = Nil
-    current_status = Query_Operation.Status.FINISHED
-    current_exec_id = Document_ID.none
-  }
+  def get_location: Option[Command] = current_state.value.location
 
   private def remove_overlay()
   {
-    current_location match {
-      case None =>
-      case Some(command) =>
-        editor.remove_overlay(command, print_function, instance :: current_query)
-        editor.flush()
+    val state = current_state.value
+    for (command <- state.location) {
+      editor.remove_overlay(command, print_function, state.instance :: state.query)
     }
   }
 
@@ -70,29 +72,31 @@
 
     /* snapshot */
 
-    val (snapshot, command_results, removed) =
-      current_location match {
+    val state0 = current_state.value
+
+    val (snapshot, command_results, results, removed) =
+      state0.location match {
         case Some(cmd) =>
           val snapshot = editor.node_snapshot(cmd.node_name)
           val command_results = snapshot.state.command_results(snapshot.version, cmd)
+          val results =
+            (for {
+              (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
+              if props.contains((Markup.INSTANCE, state0.instance))
+            } yield elem).toList
           val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
-          (snapshot, command_results, removed)
+          (snapshot, command_results, results, removed)
         case None =>
-          (Document.Snapshot.init, Command.Results.empty, true)
+          (Document.Snapshot.init, Command.Results.empty, Nil, true)
       }
 
-    val results =
-      (for {
-        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
-        if props.contains((Markup.INSTANCE, instance))
-      } yield elem).toList
 
 
     /* resolve sendback: static command id */
 
     def resolve_sendback(body: XML.Body): XML.Body =
     {
-      current_location match {
+      state0.location match {
         case None => body
         case Some(command) =>
           def resolve(body: XML.Body): XML.Body =
@@ -101,7 +105,7 @@
               case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
                 val props1 =
                   props.map({
-                    case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
+                    case (Markup.ID, Properties.Value.Long(id)) if id == state0.exec_id =>
                       (Markup.ID, Properties.Value.Long(command.id))
                     case p => p
                   })
@@ -137,27 +141,27 @@
         get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
         Query_Operation.Status.WAITING
 
+
+    /* state update */
+
     if (new_status == Query_Operation.Status.RUNNING)
       results.collectFirst(
       {
         case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
         if elem.name == Markup.RUNNING => id
-      }).foreach(id => current_exec_id = id)
-
-
-    /* state update */
+      }).foreach(id => current_state.change(_.copy(exec_id = id)))
 
-    if (current_output != new_output || current_status != new_status) {
+    if (state0.output != new_output || state0.status != new_status) {
       if (snapshot.is_outdated)
-        current_update_pending = true
+        current_state.change(_.copy(update_pending = true))
       else {
-        current_update_pending = false
-        if (current_output != new_output && !removed) {
-          current_output = new_output
+        current_state.change(_.copy(update_pending = false))
+        if (state0.output != new_output && !removed) {
+          current_state.change(_.copy(output = new_output))
           consume_output(snapshot, command_results, new_output)
         }
-        if (current_status != new_status) {
-          current_status = new_status
+        if (state0.status != new_status) {
+          current_state.change(_.copy(status = new_status))
           consume_status(new_status)
           if (new_status == Query_Operation.Status.FINISHED)
             remove_overlay()
@@ -170,7 +174,7 @@
   /* query operations */
 
   def cancel_query(): Unit =
-    GUI_Thread.require { editor.session.cancel_exec(current_exec_id) }
+    GUI_Thread.require { editor.session.cancel_exec(current_state.value.exec_id) }
 
   def apply_query(query: List[String])
   {
@@ -179,19 +183,18 @@
     editor.current_node_snapshot(editor_context) match {
       case Some(snapshot) =>
         remove_overlay()
-        reset_state()
+        current_state.change(_ => Query_Operation.State.empty)
         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
         if (!snapshot.is_outdated) {
           editor.current_command(editor_context, snapshot) match {
             case Some(command) =>
-              current_location = Some(command)
-              current_query = query
-              current_status = Query_Operation.Status.WAITING
-              editor.insert_overlay(command, print_function, instance :: query)
+              val state = Query_Operation.State.make(command, query)
+              current_state.change(_ => state)
+              editor.insert_overlay(command, print_function, state.instance :: query)
             case None =>
           }
         }
-        consume_status(current_status)
+        consume_status(current_state.value.status)
         editor.flush()
       case None =>
     }
@@ -201,8 +204,9 @@
   {
     GUI_Thread.require {}
 
+    val state = current_state.value
     for {
-      command <- current_location
+      command <- state.location
       snapshot = editor.node_snapshot(command.node_name)
       link <- editor.hyperlink_command(true, snapshot, command)
     } link.follow(editor_context)
@@ -214,10 +218,11 @@
   private val main =
     Session.Consumer[Session.Commands_Changed](getClass.getName) {
       case changed =>
-        current_location match {
+        val state = current_state.value
+        state.location match {
           case Some(command)
-          if current_update_pending ||
-            (current_status != Query_Operation.Status.FINISHED &&
+          if state.update_pending ||
+            (state.status != Query_Operation.Status.FINISHED &&
               changed.commands.contains(command)) =>
             GUI_Thread.later { content_update() }
           case _ =>
@@ -231,8 +236,8 @@
   def deactivate() {
     editor.session.commands_changed -= main
     remove_overlay()
-    reset_state()
+    current_state.change(_ => Query_Operation.State.empty)
     consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
-    consume_status(current_status)
+    consume_status(Query_Operation.Status.FINISHED)
   }
 }
diff -r 980dd46a03fb -r 933eb9e6a1cc src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/Pure/Thy/thy_info.scala	Tue Nov 03 11:20:21 2015 +0100
@@ -35,23 +35,25 @@
 
   object Dependencies
   {
-    val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty)
+    val empty = new Dependencies(Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
   }
 
   final class Dependencies private(
     rev_deps: List[Thy_Info.Dep],
     val keywords: Thy_Header.Keywords,
+    val seen: Set[Document.Node.Name],
     val seen_names: Multi_Map[String, Document.Node.Name],
     val seen_positions: Multi_Map[String, Position.T])
   {
     def :: (dep: Thy_Info.Dep): Dependencies =
       new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
-        seen_names, seen_positions)
+        seen, seen_names, seen_positions)
 
     def + (thy: (Document.Node.Name, Position.T)): Dependencies =
     {
       val (name, pos) = thy
       new Dependencies(rev_deps, keywords,
+        seen + name,
         seen_names + (name.theory -> name),
         seen_positions + (name.theory -> pos))
     }
@@ -102,15 +104,13 @@
       required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
   {
     val (name, require_pos) = thy
-    val theory = name.theory
 
     def message: String =
-      "The error(s) above occurred for theory " + quote(theory) +
+      "The error(s) above occurred for theory " + quote(name.theory) +
         required_by(initiators) + Position.here(require_pos)
 
     val required1 = required + thy
-    if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory))
-      required1
+    if (required.seen(name) || resources.loaded_theories(name.theory)) required1
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
diff -r 980dd46a03fb -r 933eb9e6a1cc src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Nov 03 11:20:21 2015 +0100
@@ -196,7 +196,10 @@
 fun output_text state {markdown} source =
   let
     val pos = Input.pos_of source;
-    val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
+    val _ =
+      Position.report pos
+        (Markup.language_document
+          {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
     val syms = Input.source_explode source;
 
     val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;
diff -r 980dd46a03fb -r 933eb9e6a1cc src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Nov 03 11:20:21 2015 +0100
@@ -255,6 +255,9 @@
       reset_blob()
       reset_bibtex()
 
+      for (doc_view <- PIDE.document_views(buffer))
+        doc_view.rich_text_area.active_reset()
+
       if (clear) {
         pending_clear = true
         pending.clear
diff -r 980dd46a03fb -r 933eb9e6a1cc src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 02 16:17:09 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 03 11:20:21 2015 +0100
@@ -41,7 +41,7 @@
         name => (name, Document.Node.no_perspective_text))
 
     val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
-    if (edits.nonEmpty) session.update(doc_blobs, edits)
+    session.update(doc_blobs, edits)
   }
 
   private val delay_flush =