# HG changeset patch
# User wenzelm
# Date 1461704365 -7200
# Node ID 60406bf310f8e9598bb08638d941a97036f5ecf3
# Parent  4a108f280dc25e292927fd32086b4d8b913f824d# Parent  21ebc2f5c571d9a2086ccdbb27af4cfb067cd778
merged

diff -r 4a108f280dc2 -r 60406bf310f8 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Fri Apr 22 17:22:29 2016 +0200
+++ b/Admin/Release/CHECKLIST	Tue Apr 26 22:59:25 2016 +0200
@@ -69,10 +69,13 @@
 Packaging
 =========
 
-- fully-automated packaging (requires Mac OS X with gnutar, avoid Mavericks):
+- fully-automated packaging:
 
   hg up -r DISTNAME && Admin/Release/build -O -l -r DISTNAME /home/isabelle/dist
 
+  Mac OS X: requires gnutar, avoid Mavericks (problems with hdiutil?)
+  Linux: avoid Debian (bitmap fonts for prog-prove)
+
 
 Final release stage
 ===================
diff -r 4a108f280dc2 -r 60406bf310f8 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Fri Apr 22 17:22:29 2016 +0200
+++ b/Admin/lib/Tools/makedist	Tue Apr 26 22:59:25 2016 +0200
@@ -180,7 +180,7 @@
 
 echo "### Preparing distribution $DISTNAME"
 
-find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
+find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -print | xargs chmod -f -x
 find . -print | xargs chmod -f u+rw
 
 export CLASSPATH="$ISABELLE_CLASSPATH"
diff -r 4a108f280dc2 -r 60406bf310f8 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Fri Apr 22 17:22:29 2016 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Tue Apr 26 22:59:25 2016 +0200
@@ -320,8 +320,13 @@
           "contrib/cygwin/isabelle/."
       done
 
-      find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
-        -print0 > "contrib/cygwin/isabelle/executables"
+      if [ "$ISABELLE_PLATFORM_FAMILY" = macos ]; then
+        find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
+          -print0 > "contrib/cygwin/isabelle/executables"
+      else
+        find . -type f -not -name '*.exe' -not -name '*.dll' -executable \
+          -print0 > "contrib/cygwin/isabelle/executables"
+      fi
 
       find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \
         > "contrib/cygwin/isabelle/symlinks"
diff -r 4a108f280dc2 -r 60406bf310f8 NEWS
--- a/NEWS	Fri Apr 22 17:22:29 2016 +0200
+++ b/NEWS	Tue Apr 26 22:59:25 2016 +0200
@@ -64,6 +64,9 @@
 'definition' and 'obtain'. It fits better into the Isar language than
 old 'def', which is now a legacy feature.
 
+* Command 'obtain' supports structured statements with 'if' / 'for'
+context.
+
 * Command '\<proof>' is an alias for 'sorry', with different
 typesetting. E.g. to produce proof holes in examples and documentation.
 
diff -r 4a108f280dc2 -r 60406bf310f8 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -1322,8 +1322,12 @@
   @{rail \<open>
     @@{command consider} @{syntax obtain_clauses}
     ;
-    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and')
-      @'where' (@{syntax props} + @'and')
+    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline>
+      @'where' concl prems @{syntax for_fixes}
+    ;
+    concl: (@{syntax props} + @'and')
+    ;
+    prems: (@'if' (@{syntax props'} + @'and'))?
     ;
     @@{command guess} (@{syntax "fixes"} + @'and')
   \<close>}
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/ContNotDenum.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -41,9 +41,10 @@
     by (auto simp add: not_le cong: conj_cong)
        (metis dense le_less_linear less_linear less_trans order_refl)
   then obtain i j where ij:
-    "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
-    "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
-    "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+      "a < b \<Longrightarrow> i a b c < j a b c"
+      "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
+      "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+    for a b c :: real
     by metis
 
   define ivl where "ivl =
@@ -78,7 +79,7 @@
     finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
       by auto
   qed (auto simp: I_def)
-  then obtain x where "\<And>n. x \<in> I n"
+  then obtain x where "x \<in> I n" for n
     by blast
   moreover from \<open>surj f\<close> obtain j where "x = f j"
     by blast
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -1483,7 +1483,7 @@
   case (real r)
   then have "\<forall>x. \<exists>q\<ge>0. g x \<le> c \<longrightarrow> (g x = ennreal q \<and> q \<le> r)"
     by (auto simp: le_ennreal_iff)
-  then obtain f where *: "\<And>x. g x \<le> c \<Longrightarrow> 0 \<le> f x" "\<And>x. g x \<le> c \<Longrightarrow> g x = ennreal (f x)" "\<And>x. g x \<le> c \<Longrightarrow> f x \<le> r"
+  then obtain f where *: "0 \<le> f x" "g x = ennreal (f x)" "f x \<le> r" if "g x \<le> c" for x
     by metis
   from ae have ae2: "\<forall>\<^sub>F x in F. c - g x = ennreal (r - f x) \<and> f x \<le> r \<and> g x = ennreal (f x) \<and> 0 \<le> f x"
   proof eventually_elim
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -1696,7 +1696,7 @@
   shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
 proof (cases "\<exists>x. \<forall>a\<in>S. a \<le> ereal x")
   case True
-  then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y"
+  then obtain y where y: "a \<le> ereal y" if "a\<in>S" for a
     by auto
   then have "\<infinity> \<notin> S"
     by force
@@ -1705,7 +1705,7 @@
     case True
     with \<open>\<infinity> \<notin> S\<close> obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
       by auto
-    obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
+    obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "(\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z" for z
     proof (atomize_elim, rule complete_real)
       show "\<exists>x. x \<in> ereal -` S"
         using x by auto
@@ -1919,7 +1919,7 @@
   assumes *: "bdd_below A" "A \<noteq> {}"
   shows "ereal (Inf A) = (INF a:A. ereal a)"
 proof (rule ereal_Inf)
-  from * obtain l u where "\<And>x. x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A"
+  from * obtain l u where "x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A" for x
     by (auto simp: bdd_below_def)
   then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u"
     by (auto intro!: INF_greatest INF_lower)
@@ -2193,7 +2193,7 @@
     by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
 next
   assume "Sup A \<noteq> -\<infinity>"
-  then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A"
+  then obtain l where "incseq l" and l: "l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A" for i :: nat
     by (auto dest: countable_approach)
 
   have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
@@ -2456,7 +2456,7 @@
   from \<open>open S\<close>
   have "open (ereal -` S)"
     by (rule ereal_openE)
-  then obtain e where "e > 0" and e: "\<And>y. dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S"
+  then obtain e where "e > 0" and e: "dist y (real_of_ereal x) < e \<Longrightarrow> ereal y \<in> S" for y
     using assms unfolding open_dist by force
   show thesis
   proof (intro that subsetI)
@@ -2830,11 +2830,12 @@
   assume "open S" and "x \<in> S"
   then have "open (ereal -` S)"
     unfolding open_ereal_def by auto
-  with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
+  with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "dist y rx < r \<Longrightarrow> ereal y \<in> S" for y
     unfolding open_dist rx by auto
-  then obtain n where
-    upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
-    lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
+  then obtain n
+    where upper: "u N < x + ereal r"
+      and lower: "x < u N + ereal r"
+      if "n \<le> N" for N
     using assms(2)[of "ereal r"] by auto
   show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
   proof (safe intro!: exI[of _ n])
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/Fun_Lexorder.thy
--- a/src/HOL/Library/Fun_Lexorder.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Fun_Lexorder.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -24,9 +24,9 @@
   assumes "less_fun f g"
   shows "\<not> less_fun g f"
 proof
-  from assms obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
+  from assms obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
     by (blast elim!: less_funE) 
-  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = f k'"
+  assume "less_fun g f" then obtain k2 where k2: "g k2 < f k2" "k' < k2 \<Longrightarrow> g k' = f k'" for k'
     by (blast elim!: less_funE) 
   show False proof (cases k1 k2 rule: linorder_cases)
     case equal with k1 k2 show False by simp
@@ -52,9 +52,9 @@
   assumes "less_fun f g" and "less_fun g h"
   shows "less_fun f h"
 proof (rule less_funI)
-  from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "\<And>k'. k' < k1 \<Longrightarrow> f k' = g k'"
-    by (blast elim!: less_funE) 
-  from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "\<And>k'. k' < k2 \<Longrightarrow> g k' = h k'"
+  from \<open>less_fun f g\<close> obtain k1 where k1: "f k1 < g k1" "k' < k1 \<Longrightarrow> f k' = g k'" for k'
+    by (blast elim!: less_funE)                          
+  from \<open>less_fun g h\<close> obtain k2 where k2: "g k2 < h k2" "k' < k2 \<Longrightarrow> g k' = h k'" for k'
     by (blast elim!: less_funE) 
   show "\<exists>k. f k < h k \<and> (\<forall>k'<k. f k' = h k')"
   proof (cases k1 k2 rule: linorder_cases)
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -96,9 +96,9 @@
   assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
   then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i"
     by auto
-  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)"
+  from bchoice[OF this] obtain n where n: "f i \<in> A (n i) i" if "i \<in> I" for i
     by auto
-  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
+  obtain k where k: "n i \<le> k" if "i \<in> I" for i
     using \<open>finite I\<close> finite_nat_set_iff_bounded_le[of "n`I"] by auto
   have "f \<in> Pi I (A k)"
   proof (intro Pi_I)
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/Function_Growth.thy
--- a/src/HOL/Library/Function_Growth.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Function_Growth.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -163,7 +163,7 @@
     and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
 proof -
   from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
-  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
+  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
     by (rule less_eq_funE) blast
   { fix c n :: nat
     assume "c > 0"
@@ -202,8 +202,8 @@
   shows "f \<prec> g"
 proof (rule less_funI)
   have "1 > (0::nat)" by simp
-  from assms \<open>1 > 0\<close> have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
-  then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
+  with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
+    by blast
   have "\<forall>m>n. f m \<le> 1 * g m"
   proof (rule allI, rule impI)
     fix m
@@ -214,7 +214,7 @@
   with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   fix c n :: nat
   assume "c > 0"
-  with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
+  with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
   then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
   moreover have "Suc (q + n) > n" by simp
   ultimately show "\<exists>m>n. c * f m < g m" by blast
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -312,7 +312,7 @@
   assumes ep: "e > 0"
   shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
 proof -
-  obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
+  obtain q where q: "degree q = degree p" "poly q x = poly p (z + x)" for x
   proof
     show "degree (offset_poly p z) = degree p"
       by (rule degree_offset_poly)
@@ -329,7 +329,7 @@
   next
     case (pCons c cs)
     from poly_bound_exists[of 1 "cs"]
-    obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m"
+    obtain m where m: "m > 0" "norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" for z
       by blast
     from ep m(1) have em0: "e/m > 0"
       by (simp add: field_simps)
@@ -535,12 +535,14 @@
   proof (cases "cs = 0")
     case False
     from poly_infinity[OF False, of "cmod (poly (pCons c cs) 0)" c]
-    obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
+    obtain r where r: "cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
+      if "r \<le> cmod z" for z
       by blast
     have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
       by arith
     from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
-    obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
+    obtain v where v: "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
+      if "cmod w \<le> \<bar>r\<bar>" for w
       by blast
     have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
       using v[of 0] r[OF z] by simp
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -2075,7 +2075,7 @@
     "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
 proof -
   from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K"
-    "\<And>b. b \<in># K \<Longrightarrow> b < a" by (blast elim: mult1E)
+    "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
   moreover from this(3) [of a] have "a \<notin># K" by auto
   ultimately show thesis by (auto intro: that)
 qed
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -3353,7 +3353,7 @@
   fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
   define cs where "cs = coeffs p"
   from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
-  then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))" 
+  then obtain f where f: "coeff p i = of_rat (f (coeff p i))" for i
     by (subst (asm) bchoice_iff) blast
   define cs' where "cs' = map (quotient_of \<circ> f) (coeffs p)"
   define d where "d = Lcm (set (map snd cs'))"
@@ -3392,9 +3392,8 @@
   moreover from root have "poly p' x = 0" by (simp add: p'_def)
   ultimately show "algebraic x" unfolding algebraic_def by blast
 next
-
   assume "algebraic x"
-  then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" 
+  then obtain p where p: "coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" for i
     by (force simp: algebraic_def)
   moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
   ultimately show  "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Library/Ramsey.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -231,8 +231,8 @@
       qed
     qed
     from dependent_choice [OF transr propr0 proprstep]
-    obtain g where pg: "!!n::nat.  ?propr (g n)"
-      and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
+    obtain g where pg: "?propr (g n)" and rg: "n<m ==> (g n, g m) \<in> ?ramr" for n m :: nat
+      by blast
     let ?gy = "fst o g"
     let ?gt = "snd o snd o g"
     have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -609,12 +609,13 @@
   next
     case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
       by simp_all
-    then obtain A B C where fact:
-      "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
+    then obtain A B C
+    where fact: "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
       and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
-      and A: "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
-      and B: "0 \<notin># B" "\<And>p. p \<in># B \<Longrightarrow> normalize p = p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
-      and C: "0 \<notin># C" "\<And>p. p \<in># C \<Longrightarrow> normalize p = p" "\<And>p. p \<in># C \<Longrightarrow> is_prime p"
+      and A: "0 \<notin># A" "p \<in># A \<Longrightarrow> normalize p = p" "p \<in># A \<Longrightarrow> is_prime p"
+      and B: "0 \<notin># B" "p \<in># B \<Longrightarrow> normalize p = p" "p \<in># B \<Longrightarrow> is_prime p"
+      and C: "0 \<notin># C" "p \<in># C \<Longrightarrow> normalize p = p" "p \<in># C \<Longrightarrow> is_prime p"
+      for p
       by (blast elim!: factorizationE)
     moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
       by simp_all
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -40,9 +40,9 @@
     by (rule types_snocE)
   from snoc have "listall ?R bs" by simp
   with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
-  then obtain bs' where
-    bsred: "\<And>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
-    and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
+  then obtain bs' where bsred: "Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
+    and bsNF: "NF (Var j \<degree>\<degree> map f bs')" for j
+    by iprover
   from snoc have "?R b" by simp
   with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
     by iprover
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -23,13 +23,13 @@
   by (rule succ_neq_zero [symmetric])
 
 
-text \<open>\medskip Primitive recursion as a (functional) relation -- polymorphic!\<close>
+text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close>
 
 inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
   for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
 where
-    Rec_zero: "Rec e r zero e"
-  | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
+  Rec_zero: "Rec e r zero e"
+| Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
 
 lemma Rec_functional:
   fixes x :: 'n
@@ -42,26 +42,30 @@
     show "\<exists>!y. ?R zero y"
     proof
       show "?R zero e" ..
-      fix y assume "?R zero y"
-      then show "y = e" by cases simp_all
+      show "y = e" if "?R zero y" for y
+        using that by cases simp_all
     qed
   next
     case (succ m)
     from \<open>\<exists>!y. ?R m y\<close>
-    obtain y where y: "?R m y"
-      and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
+    obtain y where y: "?R m y" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'"
+      by blast
     show "\<exists>!z. ?R (succ m) z"
     proof
       from y show "?R (succ m) (r m y)" ..
-      fix z assume "?R (succ m) z"
-      then obtain u where "z = r m u" and "?R m u" by cases simp_all
-      with yy' show "z = r m y" by (simp only:)
+    next
+      fix z
+      assume "?R (succ m) z"
+      then obtain u where "z = r m u" and "?R m u"
+        by cases simp_all
+      with yy' show "z = r m y"
+        by (simp only:)
     qed
   qed
 qed
 
 
-text \<open>\medskip The recursion operator -- polymorphic!\<close>
+text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>
 
 definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
   where "rec e r x = (THE y. Rec e r x y)"
@@ -86,7 +90,7 @@
 qed
 
 
-text \<open>\medskip Example: addition (monomorphic)\<close>
+text \<open>\<^medskip> Example: addition (monomorphic)\<close>
 
 definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
   where "add m n = rec n (\<lambda>_ k. succ k) m"
@@ -109,7 +113,7 @@
   by simp
 
 
-text \<open>\medskip Example: replication (polymorphic)\<close>
+text \<open>\<^medskip> Example: replication (polymorphic)\<close>
 
 definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
   where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
@@ -124,17 +128,17 @@
 end
 
 
-text \<open>\medskip Just see that our abstract specification makes sense \dots\<close>
+text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>
 
 interpretation NAT 0 Suc
 proof (rule NAT.intro)
   fix m n
   show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
   show "Suc m \<noteq> 0" by simp
-  fix P
-  assume zero: "P 0"
+  show "P n"
+    if zero: "P 0"
     and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
-  show "P n"
+    for P
   proof (induct n)
     case 0
     show ?case by (rule zero)
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/CTL.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -25,9 +25,8 @@
 
 type_synonym 'a ctl = "'a set"
 
-definition
-  imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75) where
-  "p \<rightarrow> q = - p \<union> q"
+definition imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"  (infixr "\<rightarrow>" 75)
+  where "p \<rightarrow> q = - p \<union> q"
 
 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule
@@ -43,37 +42,38 @@
 axiomatization \<M> :: "('a \<times> 'a) set"
 
 text \<open>
-  The operators \<open>\<EX>\<close>, \<open>\<EF>\<close>, \<open>\<EG>\<close> are taken as primitives, while
-  \<open>\<AX>\<close>, \<open>\<AF>\<close>, \<open>\<AG>\<close> are defined as derived ones. The formula \<open>\<EX> p\<close>
-  holds in a state @{term s}, iff there is a successor state @{term s'} (with
-  respect to the model @{term \<M>}), such that @{term p} holds in @{term s'}.
-  The formula \<open>\<EF> p\<close> holds in a state @{term s}, iff there is a path in
-  \<open>\<M>\<close>, starting from @{term s}, such that there exists a state @{term s'} on
-  the path, such that @{term p} holds in @{term s'}. The formula \<open>\<EG> p\<close>
-  holds in a state @{term s}, iff there is a path, starting from @{term s},
-  such that for all states @{term s'} on the path, @{term p} holds in @{term
-  s'}. It is easy to see that \<open>\<EF> p\<close> and \<open>\<EG> p\<close> may be expressed using
-  least and greatest fixed points @{cite "McMillan-PhDThesis"}.
+  The operators \<open>\<^bold>E\<^bold>X\<close>, \<open>\<^bold>E\<^bold>F\<close>, \<open>\<^bold>E\<^bold>G\<close> are taken as primitives, while \<open>\<^bold>A\<^bold>X\<close>,
+  \<open>\<^bold>A\<^bold>F\<close>, \<open>\<^bold>A\<^bold>G\<close> are defined as derived ones. The formula \<open>\<^bold>E\<^bold>X p\<close> holds in a
+  state \<open>s\<close>, iff there is a successor state \<open>s'\<close> (with respect to the model
+  \<open>\<M>\<close>), such that \<open>p\<close> holds in \<open>s'\<close>. The formula \<open>\<^bold>E\<^bold>F p\<close> holds in a state
+  \<open>s\<close>, iff there is a path in \<open>\<M>\<close>, starting from \<open>s\<close>, such that there exists a
+  state \<open>s'\<close> on the path, such that \<open>p\<close> holds in \<open>s'\<close>. The formula \<open>\<^bold>E\<^bold>G p\<close>
+  holds in a state \<open>s\<close>, iff there is a path, starting from \<open>s\<close>, such that for
+  all states \<open>s'\<close> on the path, \<open>p\<close> holds in \<open>s'\<close>. It is easy to see that \<open>\<^bold>E\<^bold>F
+  p\<close> and \<open>\<^bold>E\<^bold>G p\<close> may be expressed using least and greatest fixed points
+  @{cite "McMillan-PhDThesis"}.
 \<close>
 
-definition EX  ("\<EX> _" [80] 90)
-  where [simp]: "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
-definition EF ("\<EF> _" [80] 90)
-  where [simp]: "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"
-definition EG ("\<EG> _" [80] 90)
-  where [simp]: "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
+definition EX  ("\<^bold>E\<^bold>X _" [80] 90)
+  where [simp]: "\<^bold>E\<^bold>X p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
+
+definition EF ("\<^bold>E\<^bold>F _" [80] 90)
+  where [simp]: "\<^bold>E\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)"
+
+definition EG ("\<^bold>E\<^bold>G _" [80] 90)
+  where [simp]: "\<^bold>E\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)"
 
 text \<open>
-  \<open>\<AX>\<close>, \<open>\<AF>\<close> and \<open>\<AG>\<close> are now defined dually in terms of \<open>\<EX>\<close>,
-  \<open>\<EF>\<close> and \<open>\<EG>\<close>.
+  \<open>\<^bold>A\<^bold>X\<close>, \<open>\<^bold>A\<^bold>F\<close> and \<open>\<^bold>A\<^bold>G\<close> are now defined dually in terms of \<open>\<^bold>E\<^bold>X\<close>,
+  \<open>\<^bold>E\<^bold>F\<close> and \<open>\<^bold>E\<^bold>G\<close>.
 \<close>
 
-definition AX  ("\<AX> _" [80] 90)
-  where [simp]: "\<AX> p = - \<EX> - p"
-definition AF  ("\<AF> _" [80] 90)
-  where [simp]: "\<AF> p = - \<EG> - p"
-definition AG  ("\<AG> _" [80] 90)
-  where [simp]: "\<AG> p = - \<EF> - p"
+definition AX  ("\<^bold>A\<^bold>X _" [80] 90)
+  where [simp]: "\<^bold>A\<^bold>X p = - \<^bold>E\<^bold>X - p"
+definition AF  ("\<^bold>A\<^bold>F _" [80] 90)
+  where [simp]: "\<^bold>A\<^bold>F p = - \<^bold>E\<^bold>G - p"
+definition AG  ("\<^bold>A\<^bold>G _" [80] 90)
+  where [simp]: "\<^bold>A\<^bold>G p = - \<^bold>E\<^bold>F - p"
 
 
 subsection \<open>Basic fixed point properties\<close>
@@ -86,8 +86,7 @@
 proof
   show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
   proof
-    fix x assume l: "x \<in> lfp f"
-    show "x \<in> - gfp (\<lambda>s. - f (- s))"
+    show "x \<in> - gfp (\<lambda>s. - f (- s))" if l: "x \<in> lfp f" for x
     proof
       assume "x \<in> gfp (\<lambda>s. - f (- s))"
       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
@@ -100,7 +99,8 @@
   qed
   show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
   proof (rule lfp_greatest)
-    fix u assume "f u \<subseteq> u"
+    fix u
+    assume "f u \<subseteq> u"
     then have "- u \<subseteq> - f u" by auto
     then have "- u \<subseteq> - f (- (- u))" by simp
     then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
@@ -115,43 +115,44 @@
   by (simp add: lfp_gfp)
 
 text \<open>
-  In order to give dual fixed point representations of @{term "\<AF> p"} and
-  @{term "\<AG> p"}:
+  In order to give dual fixed point representations of @{term "\<^bold>A\<^bold>F p"} and
+  @{term "\<^bold>A\<^bold>G p"}:
 \<close>
 
-lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)"
-  by (simp add: lfp_gfp)
-lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)"
+lemma AF_lfp: "\<^bold>A\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)"
   by (simp add: lfp_gfp)
 
-lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
+lemma AG_gfp: "\<^bold>A\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)"
+  by (simp add: lfp_gfp)
+
+lemma EF_fp: "\<^bold>E\<^bold>F p = p \<union> \<^bold>E\<^bold>X \<^bold>E\<^bold>F p"
 proof -
-  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
+  have "mono (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)" by rule auto
   then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
 qed
 
-lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
+lemma AF_fp: "\<^bold>A\<^bold>F p = p \<union> \<^bold>A\<^bold>X \<^bold>A\<^bold>F p"
 proof -
-  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
+  have "mono (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)" by rule auto
   then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
 qed
 
-lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
+lemma EG_fp: "\<^bold>E\<^bold>G p = p \<inter> \<^bold>E\<^bold>X \<^bold>E\<^bold>G p"
 proof -
-  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
+  have "mono (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)" by rule auto
   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
 qed
 
 text \<open>
-  From the greatest fixed point definition of @{term "\<AG> p"}, we derive as
+  From the greatest fixed point definition of @{term "\<^bold>A\<^bold>G p"}, we derive as
   a consequence of the Knaster-Tarski theorem on the one hand that @{term
-  "\<AG> p"} is a fixed point of the monotonic function
-  @{term "\<lambda>s. p \<inter> \<AX> s"}.
+  "\<^bold>A\<^bold>G p"} is a fixed point of the monotonic function
+  @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"}.
 \<close>
 
-lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
+lemma AG_fp: "\<^bold>A\<^bold>G p = p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
 proof -
-  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
+  have "mono (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)" by rule auto
   then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
 qed
 
@@ -160,27 +161,27 @@
   of \<open>\<subseteq>\<close>, which is an instance of the overloaded \<open>\<le>\<close> in Isabelle/HOL).
 \<close>
 
-lemma AG_fp_1: "\<AG> p \<subseteq> p"
+lemma AG_fp_1: "\<^bold>A\<^bold>G p \<subseteq> p"
 proof -
-  note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
+  note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> p" by auto
   finally show ?thesis .
 qed
 
-lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
+lemma AG_fp_2: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
 proof -
-  note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
+  note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by auto
   finally show ?thesis .
 qed
 
 text \<open>
   On the other hand, we have from the Knaster-Tarski fixed point theorem that
-  any other post-fixed point of @{term "\<lambda>s. p \<inter> \<AX> s"} is smaller than
-  @{term "\<AG> p"}. A post-fixed point is a set of states @{term q} such that
-  @{term "q \<subseteq> p \<inter> \<AX> q"}. This leads to the following co-induction
-  principle for @{term "\<AG> p"}.
+  any other post-fixed point of @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"} is smaller than
+  @{term "\<^bold>A\<^bold>G p"}. A post-fixed point is a set of states \<open>q\<close> such that @{term
+  "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q"}. This leads to the following co-induction principle for
+  @{term "\<^bold>A\<^bold>G p"}.
 \<close>
 
-lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
+lemma AG_I: "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q \<Longrightarrow> q \<subseteq> \<^bold>A\<^bold>G p"
   by (simp only: AG_gfp) (rule gfp_upperbound)
 
 
@@ -188,92 +189,91 @@
 
 text \<open>
   With the most basic facts available, we are now able to establish a few more
-  interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<AG>\<close>
+  interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<^bold>A\<^bold>G\<close>
   (see below). We will use some elementary monotonicity and distributivity
   rules.
 \<close>
 
-lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
-lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
-lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
-  by (simp only: AG_gfp, rule gfp_mono) auto 
+lemma AX_int: "\<^bold>A\<^bold>X (p \<inter> q) = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X q" by auto
+lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X q" by auto
+lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G q"
+  by (simp only: AG_gfp, rule gfp_mono) auto
 
 text \<open>
   The formula @{term "AG p"} implies @{term "AX p"} (we use substitution of
   \<open>\<subseteq>\<close> with monotonicity).
 \<close>
 
-lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
+lemma AG_AX: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p"
 proof -
-  have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
-  also have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
+  have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
+  also have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
   moreover note AX_mono
   finally show ?thesis .
 qed
 
 text \<open>
-  Furthermore we show idempotency of the \<open>\<AG>\<close> operator. The proof is a good
+  Furthermore we show idempotency of the \<open>\<^bold>A\<^bold>G\<close> operator. The proof is a good
   example of how accumulated facts may get used to feed a single rule step.
 \<close>
 
-lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
+lemma AG_AG: "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p = \<^bold>A\<^bold>G p"
 proof
-  show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
+  show "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" by (rule AG_fp_1)
 next
-  show "\<AG> p \<subseteq> \<AG> \<AG> p"
+  show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>G p"
   proof (rule AG_I)
-    have "\<AG> p \<subseteq> \<AG> p" ..
-    moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
-    ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
+    have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" ..
+    moreover have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
+    ultimately show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" ..
   qed
 qed
 
 text \<open>
   \<^smallskip>
-  We now give an alternative characterization of the \<open>\<AG>\<close> operator, which
-  describes the \<open>\<AG>\<close> operator in an ``operational'' way by tree induction:
-  In a state holds @{term "AG p"} iff in that state holds @{term p}, and in
-  all reachable states @{term s} follows from the fact that @{term p} holds in
-  @{term s}, that @{term p} also holds in all successor states of @{term s}.
-  We use the co-induction principle @{thm [source] AG_I} to establish this in
-  a purely algebraic manner.
+  We now give an alternative characterization of the \<open>\<^bold>A\<^bold>G\<close> operator, which
+  describes the \<open>\<^bold>A\<^bold>G\<close> operator in an ``operational'' way by tree induction:
+  In a state holds @{term "AG p"} iff in that state holds \<open>p\<close>, and in all
+  reachable states \<open>s\<close> follows from the fact that \<open>p\<close> holds in \<open>s\<close>, that \<open>p\<close>
+  also holds in all successor states of \<open>s\<close>. We use the co-induction principle
+  @{thm [source] AG_I} to establish this in a purely algebraic manner.
 \<close>
 
-theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
+theorem AG_induct: "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p"
 proof
-  show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p"  (is "?lhs \<subseteq> _")
+  show "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G p"  (is "?lhs \<subseteq> _")
   proof (rule AG_I)
-    show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
+    show "?lhs \<subseteq> p \<inter> \<^bold>A\<^bold>X ?lhs"
     proof
       show "?lhs \<subseteq> p" ..
-      show "?lhs \<subseteq> \<AX> ?lhs"
+      show "?lhs \<subseteq> \<^bold>A\<^bold>X ?lhs"
       proof -
         {
-          have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
-          also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
-          finally have "?lhs \<subseteq> \<AX> p" by auto
-        }  
+          have "\<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" by (rule AG_fp_1)
+          also have "p \<inter> p \<rightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X p" ..
+          finally have "?lhs \<subseteq> \<^bold>A\<^bold>X p" by auto
+        }
         moreover
         {
-          have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
-          also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
-          finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
-        }  
-        ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
-        also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
+          have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" ..
+          also have "\<dots> \<subseteq> \<^bold>A\<^bold>X \<dots>" by (rule AG_fp_2)
+          finally have "?lhs \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" .
+        }
+        ultimately have "?lhs \<subseteq> \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" ..
+        also have "\<dots> = \<^bold>A\<^bold>X ?lhs" by (simp only: AX_int)
         finally show ?thesis .
       qed
     qed
   qed
 next
-  show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
+  show "\<^bold>A\<^bold>G p \<subseteq> p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
   proof
-    show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
-    show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
+    show "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
+    show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
     proof -
-      have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
-      also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
-      also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
+      have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
+      also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX) moreover note AG_mono
+      also have "\<^bold>A\<^bold>X p \<subseteq> (p \<rightarrow> \<^bold>A\<^bold>X p)" .. moreover note AG_mono
       finally show ?thesis .
     qed
   qed
@@ -284,30 +284,30 @@
 
 text \<open>
   Further interesting properties of CTL expressions may be demonstrated with
-  the help of tree induction; here we show that \<open>\<AX>\<close> and \<open>\<AG>\<close> commute.
+  the help of tree induction; here we show that \<open>\<^bold>A\<^bold>X\<close> and \<open>\<^bold>A\<^bold>G\<close> commute.
 \<close>
 
-theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
+theorem AG_AX_commute: "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
 proof -
-  have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
-  also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
-  also have "p \<inter> \<AG> \<AX> p = \<AG> p"  (is "?lhs = _")
-  proof  
-    have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
-    also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
+  have "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" by (rule AG_fp)
+  also have "\<dots> = \<^bold>A\<^bold>X (p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p)" by (simp only: AX_int)
+  also have "p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>G p"  (is "?lhs = _")
+  proof
+    have "\<^bold>A\<^bold>X p \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" ..
+    also have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p" by (rule AG_induct)
     also note Int_mono AG_mono
-    ultimately show "?lhs \<subseteq> \<AG> p" by fast
-  next  
-    have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
-    moreover 
+    ultimately show "?lhs \<subseteq> \<^bold>A\<^bold>G p" by fast
+  next
+    have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
+    moreover
     {
-      have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
-      also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
+      have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
+      also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX)
       also note AG_mono
-      ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
-    } 
-    ultimately show "\<AG> p \<subseteq> ?lhs" ..
-  qed  
+      ultimately have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" .
+    }
+    ultimately show "\<^bold>A\<^bold>G p \<subseteq> ?lhs" ..
+  qed
   finally show ?thesis .
 qed
 
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -13,14 +13,14 @@
 
 subsection \<open>Regular outer syntax\<close>
 
-text \<open>Text cartouches may be used in the outer syntax category "text",
-  as alternative to the traditional "verbatim" tokens.  An example is
+text \<open>Text cartouches may be used in the outer syntax category \<open>text\<close>,
+  as alternative to the traditional \<open>verbatim\<close> tokens.  An example is
   this text block.\<close>  \<comment> \<open>The same works for small side-comments.\<close>
 
 notepad
 begin
   txt \<open>Moreover, cartouches work as additional syntax in the
-    "altstring" category, for literal fact references.  For example:\<close>
+    \<open>altstring\<close> category, for literal fact references.  For example:\<close>
 
   fix x y :: 'a
   assume "x = y"
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/ex/Coherent.thy
--- a/src/HOL/ex/Coherent.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Coherent.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -16,65 +16,63 @@
   relcomp (infixr "O" 75)
 
 lemma p1p2:
-  assumes
-  "col a b c l \<and> col d e f m"
-  "col b f g n \<and> col c e g o"
-  "col b d h p \<and> col a e h q"
-  "col c d i r \<and> col a f i s"
-  "el n o \<Longrightarrow> goal"
-  "el p q \<Longrightarrow> goal"
-  "el s r \<Longrightarrow> goal"
-  "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
-  "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
-  "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
-  "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
-  "\<And>A B. pl A B \<Longrightarrow> ep A A"
-  "\<And>A B. ep A B \<Longrightarrow> ep B A"
-  "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
-  "\<And>A B. pl A B \<Longrightarrow> el B B"
-  "\<And>A B. el A B \<Longrightarrow> el B A"
-  "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
-  "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
-  "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
-  "\<And>A B C D E F G H I J K L M N O P Q.
-     col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
-     col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
-     (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
-  "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
-  "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+  assumes "col a b c l \<and> col d e f m"
+    and "col b f g n \<and> col c e g o"
+    and "col b d h p \<and> col a e h q"
+    and "col c d i r \<and> col a f i s"
+    and "el n o \<Longrightarrow> goal"
+    and "el p q \<Longrightarrow> goal"
+    and "el s r \<Longrightarrow> goal"
+    and "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+    and "\<And>A B. pl A B \<Longrightarrow> el B B"
+    and "\<And>A B. el A B \<Longrightarrow> el B A"
+    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+    and "\<And>A B C D E F G H I J K L M N O P Q.
+           col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
+           col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
+           (\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> pl G D"
+    and "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C"
+    and "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
   shows goal using assms
   by coherent
 
 lemma p2p1:
-  assumes
-  "col a b c l \<and> col d e f m"
-  "col b f g n \<and> col c e g o"
-  "col b d h p \<and> col a e h q"
-  "col c d i r \<and> col a f i s"
-  "pl a m \<Longrightarrow> goal"
-  "pl b m \<Longrightarrow> goal"
-  "pl c m \<Longrightarrow> goal"
-  "pl d l \<Longrightarrow> goal"
-  "pl e l \<Longrightarrow> goal"
-  "pl f l \<Longrightarrow> goal"
-  "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
-  "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
-  "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
-  "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
-  "\<And>A B. pl A B \<Longrightarrow> ep A A"
-  "\<And>A B. ep A B \<Longrightarrow> ep B A"
-  "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
-  "\<And>A B. pl A B \<Longrightarrow> el B B"
-  "\<And>A B. el A B \<Longrightarrow> el B A"
-  "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
-  "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
-  "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
-  "\<And>A B C D E F G H I J K L M N O P Q.
-     col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
-     col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
-     (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
-  "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
-  "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
+  assumes "col a b c l \<and> col d e f m"
+    and "col b f g n \<and> col c e g o"
+    and "col b d h p \<and> col a e h q"
+    and "col c d i r \<and> col a f i s"
+    and "pl a m \<Longrightarrow> goal"
+    and "pl b m \<Longrightarrow> goal"
+    and "pl c m \<Longrightarrow> goal"
+    and "pl d l \<Longrightarrow> goal"
+    and "pl e l \<Longrightarrow> goal"
+    and "pl f l \<Longrightarrow> goal"
+    and "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
+    and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
+    and "\<And>A B. pl A B \<Longrightarrow> ep A A"
+    and "\<And>A B. ep A B \<Longrightarrow> ep B A"
+    and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
+    and "\<And>A B. pl A B \<Longrightarrow> el B B"
+    and "\<And>A B. el A B \<Longrightarrow> el B A"
+    and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
+    and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
+    and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
+    and "\<And>A B C D E F G H I J K L M N O P Q.
+           col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
+           col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
+           (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
+    and "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B"
+    and "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
   shows goal using assms
   by coherent
 
@@ -82,16 +80,15 @@
 subsection \<open>Preservation of the Diamond Property under reflexive closure\<close>
 
 lemma diamond:
-  assumes
-  "reflexive_rewrite a b" "reflexive_rewrite a c"
-  "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
-  "\<And>A. equalish A A" 
-  "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
-  "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
-  "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
-  "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
-  "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
-  "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
+  assumes "reflexive_rewrite a b" "reflexive_rewrite a c"
+    and "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
+    and "\<And>A. equalish A A" 
+    and "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
+    and "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
+    and "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
+    and "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
+    and "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
+    and "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
   shows goal using assms
   by coherent
 
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/ex/Cubic_Quartic.thy
--- a/src/HOL/ex/Cubic_Quartic.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Cubic_Quartic.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -2,144 +2,160 @@
     Author:     Amine Chaieb
 *)
 
-section "The Cubic and Quartic Root Formulas"
+section \<open>The Cubic and Quartic Root Formulas\<close>
 
 theory Cubic_Quartic
 imports Complex_Main
 begin
 
-section "The Cubic Formula"
+section \<open>The Cubic Formula\<close>
 
 definition "ccbrt z = (SOME (w::complex). w^3 = z)"
 
 lemma ccbrt: "(ccbrt z) ^ 3 = z"
-proof-
-  from rcis_Ex obtain r a where ra: "z = rcis r a" by blast
+proof -
+  from rcis_Ex obtain r a where ra: "z = rcis r a"
+    by blast
   let ?r' = "if r < 0 then - root 3 (-r) else root 3 r"
   let ?a' = "a/3"
-  have "rcis ?r' ?a' ^ 3 = rcis r a" by (cases "r<0", simp_all add: DeMoivre2)
-  hence th: "\<exists>w. w^3 = z" unfolding ra by blast
-  from someI_ex[OF th] show ?thesis unfolding ccbrt_def by blast
+  have "rcis ?r' ?a' ^ 3 = rcis r a"
+    by (cases "r < 0") (simp_all add: DeMoivre2)
+  then have *: "\<exists>w. w^3 = z"
+    unfolding ra by blast
+  from someI_ex [OF *] show ?thesis
+    unfolding ccbrt_def by blast
 qed
 
-text "The reduction to a simpler form:"
+
+text \<open>The reduction to a simpler form:\<close>
 
 lemma cubic_reduction:
   fixes a :: complex
-  assumes H: "a \<noteq> 0 \<and> x = y - b / (3 * a) \<and>  p = (3* a * c - b^2) / (9 * a^2) \<and>  
-              q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
+  assumes
+    "a \<noteq> 0 \<and> x = y - b / (3 * a) \<and>  p = (3* a * c - b^2) / (9 * a^2) \<and>
+      q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
   shows "a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> y^3 + 3 * p * y - 2 * q = 0"
-proof-
-  from H have "3*a \<noteq> 0" "9*a^2 \<noteq> 0" "54*a^3 \<noteq> 0" by auto
-  hence th: "x = y - b / (3 * a) \<longleftrightarrow> (3*a) * x = (3*a) * y - b" 
-            "p = (3* a * c - b^2) / (9 * a^2) \<longleftrightarrow> (9 * a^2) * p = (3* a * c - b^2)"
-            "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) \<longleftrightarrow> 
-             (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)"
+proof -
+  from assms have "3 * a \<noteq> 0" "9 * a^2 \<noteq> 0" "54 * a^3 \<noteq> 0" by auto
+  then have *:
+      "x = y - b / (3 * a) \<longleftrightarrow> (3*a) * x = (3*a) * y - b"
+      "p = (3* a * c - b^2) / (9 * a^2) \<longleftrightarrow> (9 * a^2) * p = (3* a * c - b^2)"
+      "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) \<longleftrightarrow>
+        (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)"
     by (simp_all add: field_simps)
-  from H[unfolded th] show ?thesis by algebra
+  from assms [unfolded *] show ?thesis
+    by algebra
 qed
 
-text "The solutions of the special form:"
 
-lemma cubic_basic: 
+text \<open>The solutions of the special form:\<close>
+
+lemma cubic_basic:
   fixes s :: complex
-  assumes H: "s^2 = q^2 + p^3 \<and>
-              s1^3 = (if p = 0 then 2 * q else q + s) \<and>
-              s2 = -s1 * (1 + i * t) / 2 \<and>
-              s3 = -s1 * (1 - i * t) / 2 \<and>
-              i^2 + 1 = 0 \<and>
-              t^2 = 3"
-  shows 
+  assumes
+    "s^2 = q^2 + p^3 \<and>
+      s1^3 = (if p = 0 then 2 * q else q + s) \<and>
+      s2 = -s1 * (1 + i * t) / 2 \<and>
+      s3 = -s1 * (1 - i * t) / 2 \<and>
+      i^2 + 1 = 0 \<and>
+      t^2 = 3"
+  shows
     "if p = 0
      then y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> y = s1 \<or> y = s2 \<or> y = s3
      else s1 \<noteq> 0 \<and>
-          (y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> (y = s1 - p / s1 \<or> y = s2 - p / s2 \<or> y = s3 - p / s3))"
-proof-
- { assume p0: "p = 0"
-   with H have ?thesis by (simp add: field_simps) algebra
- }
- moreover
- { assume p0: "p \<noteq> 0"
-   with H have th1: "s1 \<noteq> 0" by (simp add: field_simps) algebra
-   from p0 H th1 have th0: "s2 \<noteq> 0" "s3 \<noteq>0"
-     by (simp_all add: field_simps) algebra+
-   from th1 th0 
-   have th: "y = s1 - p / s1 \<longleftrightarrow> s1*y = s1^2 - p"
-            "y = s2 - p / s2 \<longleftrightarrow> s2*y = s2^2 - p"
-            "y = s3 - p / s3 \<longleftrightarrow> s3*y = s3^2 - p"
-     by (simp_all add: field_simps power2_eq_square) 
-   from p0 H have ?thesis unfolding th by (simp add: field_simps) algebra
- }
- ultimately show ?thesis by blast
+      (y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> (y = s1 - p / s1 \<or> y = s2 - p / s2 \<or> y = s3 - p / s3))"
+proof (cases "p = 0")
+  case True
+  with assms show ?thesis
+    by (simp add: field_simps) algebra
+next
+  case False
+  with assms have *: "s1 \<noteq> 0" by (simp add: field_simps) algebra
+  with assms False have "s2 \<noteq> 0" "s3 \<noteq> 0"
+    by (simp_all add: field_simps) algebra+
+  with * have **:
+      "y = s1 - p / s1 \<longleftrightarrow> s1 * y = s1^2 - p"
+      "y = s2 - p / s2 \<longleftrightarrow> s2 * y = s2^2 - p"
+      "y = s3 - p / s3 \<longleftrightarrow> s3 * y = s3^2 - p"
+    by (simp_all add: field_simps power2_eq_square)
+  from assms False show ?thesis
+    unfolding ** by (simp add: field_simps) algebra
 qed
 
-text "Explicit formula for the roots:"
+
+text \<open>Explicit formula for the roots:\<close>
 
 lemma cubic:
   assumes a0: "a \<noteq> 0"
-  shows "
-  let p = (3 * a * c - b^2) / (9 * a^2) ;
+  shows
+    "let
+      p = (3 * a * c - b^2) / (9 * a^2);
       q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3);
       s = csqrt(q^2 + p^3);
       s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s));
       s2 = -s1 * (1 + ii * csqrt 3) / 2;
       s3 = -s1 * (1 - ii * csqrt 3) / 2
-  in if p = 0 then 
-       a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
-           x = s1 - b / (3 * a) \<or>
-           x = s2 - b / (3 * a) \<or>
-           x = s3 - b / (3 * a)
+     in
+      if p = 0 then
+        a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
+          x = s1 - b / (3 * a) \<or>
+          x = s2 - b / (3 * a) \<or>
+          x = s3 - b / (3 * a)
       else
         s1 \<noteq> 0 \<and>
-        (a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
+          (a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
             x = s1 - p / s1 - b / (3 * a) \<or>
             x = s2 - p / s2 - b / (3 * a) \<or>
             x = s3 - p / s3 - b / (3 * a))"
-proof-
+proof -
   let ?p = "(3 * a * c - b^2) / (9 * a^2)"
   let ?q = "(9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
-  let ?s = "csqrt(?q^2 + ?p^3)"
+  let ?s = "csqrt (?q^2 + ?p^3)"
   let ?s1 = "if ?p = 0 then ccbrt(2 * ?q) else ccbrt(?q + ?s)"
   let ?s2 = "- ?s1 * (1 + ii * csqrt 3) / 2"
   let ?s3 = "- ?s1 * (1 - ii * csqrt 3) / 2"
   let ?y = "x + b / (3 * a)"
-  from a0 have zero: "9 * a^2 \<noteq> 0" "a^3 * 54 \<noteq> 0" "(a*3)\<noteq> 0" by auto
-  have eq:"a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> ?y^3 + 3 * ?p * ?y - 2 * ?q = 0"
+  from a0 have zero: "9 * a^2 \<noteq> 0" "a^3 * 54 \<noteq> 0" "(a * 3) \<noteq> 0"
+    by auto
+  have eq: "a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> ?y^3 + 3 * ?p * ?y - 2 * ?q = 0"
     by (rule cubic_reduction) (auto simp add: field_simps zero a0)
   have "csqrt 3^2 = 3" by (rule power2_csqrt)
-  hence th0: "?s^2 = ?q^2 + ?p ^ 3 \<and> ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \<and>
-              ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \<and> 
-              ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \<and> 
-              ii^2 + 1 = 0 \<and> csqrt 3^2 = 3"
+  then have th0:
+    "?s^2 = ?q^2 + ?p ^ 3 \<and> ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \<and>
+      ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \<and>
+      ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \<and>
+      ii^2 + 1 = 0 \<and> csqrt 3^2 = 3"
     using zero by (simp add: field_simps ccbrt)
   from cubic_basic[OF th0, of ?y]
-  show ?thesis 
+  show ?thesis
     apply (simp only: Let_def eq)
     using zero apply (simp add: field_simps ccbrt)
     using zero
-    apply (cases "a * (c * 3) = b^2", simp_all add: field_simps)
+    apply (cases "a * (c * 3) = b^2")
+    apply (simp_all add: field_simps)
     done
 qed
 
 
-section "The Quartic Formula"
+section \<open>The Quartic Formula\<close>
 
 lemma quartic:
- "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 \<and>
-  R^2 = a^2 / 4 - b + y \<and>
-  s^2 = y^2 - 4 * d \<and>
-  (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
-                   else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) \<and>
-  (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
-                   else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
+  "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 \<and>
+    R^2 = a^2 / 4 - b + y \<and>
+    s^2 = y^2 - 4 * d \<and>
+    (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
+                     else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) \<and>
+    (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
+                     else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
   \<Longrightarrow> x^4 + a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
       x = -a / 4 + R / 2 + D / 2 \<or>
       x = -a / 4 + R / 2 - D / 2 \<or>
       x = -a / 4 - R / 2 + E / 2 \<or>
       x = -a / 4 - R / 2 - E / 2"
-apply (cases "R=0", simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left)
- apply algebra
-apply algebra
-done
+  apply (cases "R = 0")
+   apply (simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left)
+   apply algebra
+  apply algebra
+  done
 
 end
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -133,7 +133,7 @@
   proof (cases "b < x")
     case True
     with 2 obtain N where *: "N < length D"
-      and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
+      and **: "D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" for d t e by auto
     hence "Suc N < length ((a,t,b)#D) \<and>
            (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
     thus ?thesis by auto
@@ -372,11 +372,11 @@
   hence "a < b" and "b < c" by auto
 
   obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
-    and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
+    and I1: "fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" for D
     using IntegralE [OF \<open>Integral (a, b) f x1\<close> \<open>0 < \<epsilon>/2\<close>] by auto
 
   obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
-    and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
+    and I2: "fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" for D
     using IntegralE [OF \<open>Integral (b, c) f x2\<close> \<open>0 < \<epsilon>/2\<close>] by auto
 
   define \<delta> where "\<delta> x =
@@ -541,7 +541,7 @@
     then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
       by (simp add: DERIV_iff2 LIM_eq)
     with \<open>0 < e\<close> obtain s
-    where "\<And>z. z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
+    where "z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s" for z
       by (drule_tac x="e/2" in spec, auto)
     with strad1 [of x s f f' e] have strad:
         "\<And>z. \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
@@ -586,8 +586,8 @@
 
     from lemma_straddle [OF f' this]
     obtain \<delta> where "gauge {a..b} \<delta>"
-      and \<delta>: "\<And>x u v. \<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
-           \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
+      and \<delta>: "\<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
+           \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" for x u v by auto
 
     have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
     proof (clarify)
diff -r 4a108f280dc2 -r 60406bf310f8 src/HOL/ex/document/root.tex
--- a/src/HOL/ex/document/root.tex	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/HOL/ex/document/root.tex	Tue Apr 26 22:59:25 2016 +0200
@@ -10,14 +10,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
-\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
-\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
-\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
-\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
-\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
-
-
 
 \begin{document}
 
diff -r 4a108f280dc2 -r 60406bf310f8 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Apr 26 22:59:25 2016 +0200
@@ -15,8 +15,10 @@
   val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
   val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
   val obtain: binding -> (binding * typ option * mixfix) list ->
+    (binding * typ option * mixfix) list -> (term * term list) list list ->
     (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val obtain_cmd: binding -> (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list -> (string * string list) list list ->
     (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     ((string * cterm) list * thm list) * Proof.context
@@ -193,28 +195,32 @@
 
 local
 
-fun gen_obtain prep_spec prep_att that_binding raw_vars raw_asms int state =
+fun gen_obtain prep_stmt prep_att that_binding raw_decls raw_fixes raw_prems raw_concls int state =
   let
     val _ = Proof.assert_forward_or_chain state;
 
     val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
 
-    val (((vars, xs, params), propss, binds, binds'), params_ctxt) =
-      prep_spec raw_vars (map #2 raw_asms) thesis_ctxt;
-    val cparams = map (Thm.cterm_of params_ctxt) params;
-    val asms =
-      map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_asms ~~
-      map (map (rpair [])) propss;
+    val ((vars, propss, binds, binds'), params_ctxt) =
+      prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt;
+    val (decls, fixes) = chop (length raw_decls) vars ||> map #2;
+    val (premss, conclss) = chop (length raw_prems) propss;
+    val propss' = (map o map) (Logic.close_prop fixes (flat premss)) conclss;
 
     val that_prop =
-      Logic.list_rename_params xs
-        (fold_rev Logic.all params (Logic.list_implies (flat propss, thesis)));
+      Logic.list_rename_params (map (#1 o #2) decls)
+        (fold_rev (Logic.all o #2 o #2) decls (Logic.list_implies (flat propss', thesis)));
+
+    val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) decls;
+    val asms =
+      map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_concls ~~
+      map (map (rpair [])) propss';
 
     fun after_qed (result_ctxt, results) state' =
       let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in
         state'
-        |> Proof.fix vars
-        |> Proof.map_context (fold Variable.bind_term binds)
+        |> Proof.fix (map #1 decls)
+        |> Proof.map_context (fold (Variable.bind_term o apsnd (Logic.close_term fixes)) binds)
         |> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms
       end;
   in
@@ -229,8 +235,8 @@
 
 in
 
-val obtain = gen_obtain Proof_Context.cert_spec (K I);
-val obtain_cmd = gen_obtain Proof_Context.read_spec Attrib.attribute_cmd;
+val obtain = gen_obtain Proof_Context.cert_stmt (K I);
+val obtain_cmd = gen_obtain Proof_Context.read_stmt Attrib.attribute_cmd;
 
 end;
 
diff -r 4a108f280dc2 -r 60406bf310f8 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 26 22:59:25 2016 +0200
@@ -641,66 +641,18 @@
 end;
 
 
-(* structured clause *)
-
-fun export_binds ctxt' ctxt binds =
-  let
-    val rhss =
-      map (the_list o snd) binds
-      |> burrow (Variable.export_terms ctxt' ctxt)
-      |> map (try the_single);
-  in map fst binds ~~ rhss end;
-
-fun prep_clause prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
-  let
-    (*fixed variables*)
-    val ((xs', vars), fix_ctxt) = ctxt
-      |> fold_map prep_var raw_fixes
-      |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
-
-    (*propositions with term bindings*)
-    val (all_propss, binds) = prep_propp fix_ctxt (raw_assumes @ raw_shows);
-    val (assumes_propss, shows_propss) = chop (length raw_assumes) all_propss;
-
-    (*params*)
-    val (ps, params_ctxt) = fix_ctxt
-      |> (fold o fold) Variable.declare_term all_propss
-      |> fold Variable.bind_term binds
-      |> fold_map Proof_Context.inferred_param xs';
-    val xs = map (Variable.check_name o #1) vars;
-    val params = xs ~~ map Free ps;
-
-    val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
-
-    (*result term bindings*)
-    val shows_props = flat shows_propss;
-    val binds' =
-      (case try List.last shows_props of
-        NONE => []
-      | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
-    val result_binds =
-      (Auto_Bind.facts params_ctxt shows_props @ binds')
-      |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
-      |> export_binds params_ctxt ctxt;
-  in ((params, assumes_propss, shows_propss, result_binds), params_ctxt) end;
-
-
 (* assume *)
 
 local
 
-fun gen_assume prep_var prep_propp prep_att export raw_fixes raw_prems raw_concls state =
+fun gen_assume prep_statement prep_att export raw_fixes raw_prems raw_concls state =
   let
     val ctxt = context_of state;
 
     val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
-    val (params, prems_propss, concl_propss, result_binds) =
-      #1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt);
-
-    fun close prop =
-      fold_rev Logic.dependent_all_name params
-        (Logic.list_implies (flat prems_propss, prop));
-    val propss = (map o map) close concl_propss;
+    val ((params, prems_propss, concl_propss, result_binds), _) =
+      prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt;
+    val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
   in
     state
     |> assert_forward
@@ -716,8 +668,8 @@
 
 in
 
-val assm = gen_assume Proof_Context.cert_var Proof_Context.cert_propp (K I);
-val assm_cmd = gen_assume Proof_Context.read_var Proof_Context.read_propp Attrib.attribute_cmd;
+val assm = gen_assume Proof_Context.cert_statement (K I);
+val assm_cmd = gen_assume Proof_Context.read_statement Attrib.attribute_cmd;
 
 val assume = assm Assumption.assume_export;
 val assume_cmd = assm_cmd Assumption.assume_export;
@@ -893,45 +845,37 @@
 
 local
 
-fun match_defs (((b, _, mx), x) :: more_decls) ((((a, _), t), _) :: more_defs) =
-      if x = a then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
-      else error ("Mismatch of declaration " ^ quote x ^ " wrt. definition " ^ quote a)
-  | match_defs [] [] = []
-  | match_defs more_decls more_defs =
-      error ("Mismatch of declarations " ^ commas_quote (map #2 more_decls) ^
-        (if null more_decls then "" else " ") ^
-        "wrt. definitions " ^ commas_quote (map (#1 o #1 o #1) more_defs));
-
-fun invisible_fixes vars ctxt = ctxt
-  |> Context_Position.set_visible false
-  |> Proof_Context.add_fixes vars |> #2
-  |> Context_Position.restore_visible ctxt;
-
-fun gen_define prep_spec prep_att raw_vars raw_fixes raw_defs state =
+fun gen_define prep_stmt prep_att raw_decls raw_fixes raw_defs state =
   let
     val _ = assert_forward state;
     val ctxt = context_of state;
 
     (*vars*)
-    val n_vars = length raw_vars;
-    val (((all_vars, _, all_params), defss, _, binds'), _) =
-      prep_spec (raw_vars @ raw_fixes) (map snd raw_defs) ctxt;
-    val (vars, fixes) = chop n_vars all_vars;
-    val (params, _) = chop n_vars all_params;
+    val ((vars, propss, _, binds'), vars_ctxt) =
+      prep_stmt (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
+    val (decls, fixes) = chop (length raw_decls) vars;
+    val show_term = Syntax.string_of_term vars_ctxt;
 
     (*defs*)
-    val derived_def = Local_Defs.derived_def (invisible_fixes vars ctxt) {conditional = false};
-    val defs1 = map derived_def (flat defss);
-    val defs2 = match_defs (vars ~~ map (#1 o dest_Free) params) defs1;
+    fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) =
+          if x = y then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
+          else
+            error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^
+              show_term (Free (y, U)))
+      | match_defs [] [] = []
+      | match_defs more_decls more_defs =
+          error ("Mismatch of declarations " ^ commas (map (show_term o #2 o #2) more_decls) ^
+            (if null more_decls then "" else " ") ^
+            "wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs));
+
+    val derived_def = Local_Defs.derived_def ctxt {conditional = false};
+    val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss);
+    val defs2 = match_defs decls defs1;
     val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
 
-    (*fixes*)
-    val fixes_ctxt = invisible_fixes fixes defs_ctxt;
-    val export = singleton (Variable.export fixes_ctxt defs_ctxt);
-
     (*notes*)
     val def_thmss =
-      map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, export (prove fixes_ctxt th)))
+      map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, prove defs_ctxt th))
         (defs1 ~~ defs2 ~~ defs3)
       |> unflat (map snd raw_defs);
     val notes =
@@ -947,8 +891,8 @@
 
 in
 
-val define = gen_define Proof_Context.cert_spec (K I);
-val define_cmd = gen_define Proof_Context.read_spec Attrib.attribute_cmd;
+val define = gen_define Proof_Context.cert_stmt (K I);
+val define_cmd = gen_define Proof_Context.read_stmt Attrib.attribute_cmd;
 
 end;
 
@@ -1128,7 +1072,7 @@
 
 (* local goals *)
 
-fun local_goal print_results prep_att prep_propp prep_var strict_asm
+fun local_goal print_results prep_statement prep_att strict_asm
     kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
   let
     val ctxt = context_of state;
@@ -1139,7 +1083,7 @@
 
     (*params*)
     val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt
-      |> prep_clause prep_var prep_propp raw_fixes (map snd raw_assumes) (map snd raw_shows);
+      |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
 
     (*prems*)
     val (assumes_bindings, shows_bindings) =
@@ -1254,18 +1198,16 @@
 (* common goal statements *)
 
 fun internal_goal print_results mode =
-  local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode)
-    Proof_Context.cert_var;
+  local_goal print_results
+    (fn a => fn b => fn c => Proof_Context.cert_statement a b c o Proof_Context.set_mode mode) (K I);
 
 local
 
-fun gen_have prep_att prep_propp prep_var
-    strict_asm before_qed after_qed fixes assumes shows int =
+fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int =
   local_goal (Proof_Display.print_results int (Position.thread_data ()))
-    prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows;
+    prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows;
 
-fun gen_show prep_att prep_propp prep_var
-    strict_asm before_qed after_qed fixes assumes shows int state =
+fun gen_show prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int state =
   let
     val testing = Unsynchronized.ref false;
     val rule = Unsynchronized.ref (NONE: thm option);
@@ -1296,7 +1238,7 @@
       |> after_qed (result_ctxt, results);
   in
     state
-    |> local_goal print_results prep_att prep_propp prep_var strict_asm
+    |> local_goal print_results prep_statement prep_att strict_asm
       "show" before_qed after_qed' fixes assumes shows
     ||> int ? (fn goal_state =>
       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
@@ -1306,10 +1248,10 @@
 
 in
 
-val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var;
-val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
-val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var;
-val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
+val have = gen_have Proof_Context.cert_statement (K I);
+val have_cmd = gen_have Proof_Context.read_statement Attrib.attribute_cmd;
+val show = gen_show Proof_Context.cert_statement (K I);
+val show_cmd = gen_show Proof_Context.read_statement Attrib.attribute_cmd;
 
 end;
 
diff -r 4a108f280dc2 -r 60406bf310f8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 26 22:59:25 2016 +0200
@@ -166,12 +166,22 @@
   val generic_add_abbrev: string -> binding * term -> Context.generic ->
     (term * term) * Context.generic
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
-  val cert_spec: (binding * typ option * mixfix) list -> (term * term list) list list ->
-    Proof.context -> (((binding * typ option * mixfix) list * string list * term list) *
-      term list list * (indexname * term) list * (indexname * term) list) * Proof.context
-  val read_spec: (binding * string option * mixfix) list -> (string * string list) list list ->
-    Proof.context -> (((binding * typ option * mixfix) list * string list * term list) *
-      term list list * (indexname * term) list * (indexname * term) list) * Proof.context
+  val cert_stmt:
+    (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context ->
+    (((binding * typ option * mixfix) * (string * term)) list * term list list *
+      (indexname * term) list * (indexname * term) list) * Proof.context
+  val read_stmt:
+    (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context ->
+    (((binding * typ option * mixfix) * (string * term)) list * term list list *
+      (indexname * term) list * (indexname * term) list) * Proof.context
+  val cert_statement: (binding * typ option * mixfix) list ->
+    (term * term list) list list -> (term * term list) list list -> Proof.context ->
+    ((string * term) list * term list list * term list list * (indexname * term option) list) *
+      Proof.context
+  val read_statement: (binding * string option * mixfix) list ->
+    (string * string list) list list -> (string * string list) list list -> Proof.context ->
+    ((string * term) list * term list list * term list list * (indexname * term option) list) *
+      Proof.context
   val print_syntax: Proof.context -> unit
   val print_abbrevs: bool -> Proof.context -> unit
   val pretty_term_bindings: Proof.context -> Pretty.T list
@@ -1326,38 +1336,60 @@
 end;
 
 
-(* specification with parameters *)
+(* structured statements *)
 
 local
 
-fun prep_spec prep_var prep_propp raw_vars raw_propps ctxt =
+fun export_binds ctxt' ctxt params binds =
+  let
+    val rhss =
+      map (the_list o Option.map (Logic.close_term params) o snd) binds
+      |> burrow (Variable.export_terms ctxt' ctxt)
+      |> map (try the_single);
+  in map fst binds ~~ rhss end;
+
+fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt =
   let
-    (*vars*)
-    val ((xs', vars), vars_ctxt) = ctxt
-      |> fold_map prep_var raw_vars
-      |-> (fn vars => add_fixes vars ##>> pair vars);
+    val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
     val xs = map (Variable.check_name o #1) vars;
+    val (xs', fixes_ctxt) = add_fixes vars vars_ctxt;
 
-    (*propps*)
-    val (propss, binds) = prep_propp vars_ctxt raw_propps;
-    val props = flat propss;
+    val (propss, binds) = prep_propp fixes_ctxt raw_propps;
+    val (ps, params_ctxt) = fixes_ctxt
+      |> (fold o fold) Variable.declare_term propss
+      |> fold_map inferred_param xs';
+    val params = xs ~~ map Free ps;
 
-    (*params*)
-    val (ps, params_ctxt) = vars_ctxt
-      |> fold Variable.declare_term props
-      |> fold Variable.bind_term binds
-      |> fold_map inferred_param xs';
-    val params = map Free ps;
-    val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
     val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
+    val binds' = binds
+      |> map (apsnd SOME)
+      |> export_binds params_ctxt ctxt params
+      |> map (apsnd the);
 
-    val _ = Variable.warn_extra_tfrees vars_ctxt params_ctxt;
-  in (((vars', xs, params), propss, binds, binds'), params_ctxt) end;
+    val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
+  in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end;
+
+fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
+  let
+    val ((fixes, (assumes, shows), binds), ctxt') = ctxt
+      |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
+      |-> (fn (vars, propss, binds, _) =>
+        fold Variable.bind_term binds #>
+        pair (map #2 vars, chop (length raw_assumes) propss, binds));
+    val binds' =
+      (Auto_Bind.facts ctxt' (flat shows) @
+        (case try List.last (flat shows) of
+          NONE => []
+        | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds))
+      |> export_binds ctxt' ctxt fixes;
+  in ((fixes, assumes, shows, binds'), ctxt') end;
 
 in
 
-val cert_spec = prep_spec cert_var cert_propp;
-val read_spec = prep_spec read_var read_propp;
+val cert_stmt = prep_stmt cert_var cert_propp;
+val read_stmt = prep_stmt read_var read_propp;
+val cert_statement = prep_statement cert_var cert_propp;
+val read_statement = prep_statement read_var read_propp;
 
 end;
 
diff -r 4a108f280dc2 -r 60406bf310f8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Apr 26 22:59:25 2016 +0200
@@ -758,8 +758,8 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
-    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
-      >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
+    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement
+      >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
 
 val _ =
   Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
diff -r 4a108f280dc2 -r 60406bf310f8 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Apr 22 17:22:29 2016 +0200
+++ b/src/Pure/logic.ML	Tue Apr 26 22:59:25 2016 +0200
@@ -26,6 +26,8 @@
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term -> int
   val nth_prem: int * term -> term
+  val close_term: (string * term) list -> term -> term
+  val close_prop: (string * term) list -> term list -> term -> term
   val true_prop: term
   val conjunction: term
   val mk_conjunction: term * term -> term
@@ -147,7 +149,6 @@
 end;
 
 
-
 (** equality **)
 
 fun mk_equals (t, u) =
@@ -204,6 +205,11 @@
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
 
 
+(* close *)
+
+val close_term = fold_rev Term.dependent_lambda_name;
+fun close_prop xs As B = fold_rev dependent_all_name xs (list_implies (As, B));
+
 
 (** conjunction **)