# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1448979565 0
# Node ID 96d2c1b9a30a62f97f3e1acf43aedb03b3824620
# Parent  d50b993b4fb93c2e357936572400b3686f5b6aad# Parent  164eeb2ab675bdbf03f3be1b226ce1e01a3612c6
Merge

diff -r d50b993b4fb9 -r 96d2c1b9a30a src/FOL/ex/First_Order_Logic.thy
--- a/src/FOL/ex/First_Order_Logic.thy	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/FOL/ex/First_Order_Logic.thy	Tue Dec 01 14:19:25 2015 +0000
@@ -1,113 +1,121 @@
 (*  Title:      FOL/ex/First_Order_Logic.thy
-    Author:     Markus Wenzel, TU Munich
+    Author:     Makarius
 *)
 
 section \<open>A simple formulation of First-Order Logic\<close>
 
-theory First_Order_Logic imports Pure begin
-
 text \<open>
-  The subsequent theory development illustrates single-sorted
-  intuitionistic first-order logic with equality, formulated within
-  the Pure framework.  Actually this is not an example of
-  Isabelle/FOL, but of Isabelle/Pure.
+  The subsequent theory development illustrates single-sorted intuitionistic
+  first-order logic with equality, formulated within the Pure framework. So
+  this is strictly speaking an example of Isabelle/Pure, not Isabelle/FOL.
 \<close>
 
-subsection \<open>Syntax\<close>
+theory First_Order_Logic
+imports Pure
+begin
+
+subsection \<open>Abstract syntax\<close>
 
 typedecl i
 typedecl o
 
-judgment
-  Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
+judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
 
 
 subsection \<open>Propositional logic\<close>
 
-axiomatization
-  false :: o  ("\<bottom>") and
-  imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25) and
-  conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) and
-  disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
-where
-  falseE [elim]: "\<bottom> \<Longrightarrow> A" and
+axiomatization false :: o  ("\<bottom>")
+  where falseE [elim]: "\<bottom> \<Longrightarrow> A"
+
 
-  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
-  mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
+  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+    and mp [dest]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+
 
-  conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" and
-  conjD1: "A \<and> B \<Longrightarrow> A" and
-  conjD2: "A \<and> B \<Longrightarrow> B" and
-
-  disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C" and
-  disjI1 [intro]: "A \<Longrightarrow> A \<or> B" and
-  disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
+axiomatization conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
+  where conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
+    and conjD1: "A \<and> B \<Longrightarrow> A"
+    and conjD2: "A \<and> B \<Longrightarrow> B"
 
 theorem conjE [elim]:
   assumes "A \<and> B"
   obtains A and B
 proof
-  from \<open>A \<and> B\<close> show A by (rule conjD1)
-  from \<open>A \<and> B\<close> show B by (rule conjD2)
+  from \<open>A \<and> B\<close> show A
+    by (rule conjD1)
+  from \<open>A \<and> B\<close> show B
+    by (rule conjD2)
 qed
 
+
+axiomatization disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
+  where disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
+    and disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
+    and disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
+
+
 definition true :: o  ("\<top>")
   where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
 
+theorem trueI [intro]: \<top>
+  unfolding true_def ..
+
+
 definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
   where "\<not> A \<equiv> A \<longrightarrow> \<bottom>"
 
-definition iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25)
-  where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
-
-
-theorem trueI [intro]: \<top>
-proof (unfold true_def)
-  show "\<bottom> \<longrightarrow> \<bottom>" ..
-qed
-
 theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
-proof (unfold not_def)
-  assume "A \<Longrightarrow> \<bottom>"
-  then show "A \<longrightarrow> \<bottom>" ..
-qed
+  unfolding not_def ..
 
 theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
-proof (unfold not_def)
+  unfolding not_def
+proof -
   assume "A \<longrightarrow> \<bottom>" and A
   then have \<bottom> ..
   then show B ..
 qed
 
-theorem iffI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
-proof (unfold iff_def)
-  assume "A \<Longrightarrow> B" then have "A \<longrightarrow> B" ..
-  moreover assume "B \<Longrightarrow> A" then have "B \<longrightarrow> A" ..
-  ultimately show "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)" ..
+
+definition iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25)
+  where "A \<longleftrightarrow> B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+
+theorem iffI [intro]:
+  assumes "A \<Longrightarrow> B"
+    and "B \<Longrightarrow> A"
+  shows "A \<longleftrightarrow> B"
+  unfolding iff_def
+proof
+  from \<open>A \<Longrightarrow> B\<close> show "A \<longrightarrow> B" ..
+  from \<open>B \<Longrightarrow> A\<close> show "B \<longrightarrow> A" ..
 qed
 
-theorem iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
-proof (unfold iff_def)
-  assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+theorem iff1 [elim]:
+  assumes "A \<longleftrightarrow> B" and A
+  shows B
+proof -
+  from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+    unfolding iff_def .
   then have "A \<longrightarrow> B" ..
-  then show "A \<Longrightarrow> B" ..
+  from this and \<open>A\<close> show B ..
 qed
 
-theorem iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
-proof (unfold iff_def)
-  assume "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+theorem iff2 [elim]:
+  assumes "A \<longleftrightarrow> B" and B
+  shows A
+proof -
+  from \<open>A \<longleftrightarrow> B\<close> have "(A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
+    unfolding iff_def .
   then have "B \<longrightarrow> A" ..
-  then show "B \<Longrightarrow> A" ..
+  from this and \<open>B\<close> show A ..
 qed
 
 
 subsection \<open>Equality\<close>
 
-axiomatization
-  equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl "=" 50)
-where
-  refl [intro]: "x = x" and
-  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
+axiomatization equal :: "i \<Rightarrow> i \<Rightarrow> o"  (infixl "=" 50)
+  where refl [intro]: "x = x"
+    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
 
 theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
   by (rule subst)
@@ -115,43 +123,38 @@
 theorem sym [sym]: "x = y \<Longrightarrow> y = x"
 proof -
   assume "x = y"
-  from this and refl show "y = x" by (rule subst)
+  from this and refl show "y = x"
+    by (rule subst)
 qed
 
 
 subsection \<open>Quantifiers\<close>
 
-axiomatization
-  All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) and
-  Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
-where
-  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
-  allD [dest]: "\<forall>x. P x \<Longrightarrow> P a" and
-  exI [intro]: "P a \<Longrightarrow> \<exists>x. P x" and
-  exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
+axiomatization All :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
+  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
+    and allD [dest]: "\<forall>x. P x \<Longrightarrow> P a"
+
+axiomatization Ex :: "(i \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+  where exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
+    and exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
 
 
 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
-    fix x assume "P (f x)"
-    then show ?thesis ..
-  qed
+  then obtain x where "P (f x)" ..
+  then show "\<exists>y. P y" ..
 qed
 
 lemma "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
 proof
   assume "\<exists>x. \<forall>y. R x y"
-  then show "\<forall>y. \<exists>x. R x y"
+  then obtain x where "\<forall>y. R x y" ..
+  show "\<forall>y. \<exists>x. R x y"
   proof
-    fix x assume a: "\<forall>y. R x y"
-    show ?thesis
-    proof
-      fix y from a have "R x y" ..
-      then show "\<exists>x. R x y" ..
-    qed
+    fix y
+    from \<open>\<forall>y. R x y\<close> have "R x y" ..
+    then show "\<exists>x. R x y" ..
   qed
 qed
 
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -181,7 +181,8 @@
     val CCA = mk_T_of_bnf oDs CAs outer;
     val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners;
     val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
-    val inner_setss = @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
+    val inner_setss =
+      @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
     val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners;
     val outer_bd = mk_bd_of_bnf oDs CAs outer;
 
@@ -692,7 +693,8 @@
     val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) =
       normalize_bnfs qualify Ass Ds flatten_tyargs inners accum;
 
-    val Ds = oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
+    val Ds =
+      oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
     val As = map TFree As;
   in
     apfst (rpair (Ds, As))
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_comp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -74,14 +74,16 @@
      map (fn thm => rtac ctxt (thm RS fun_cong)) set_map0s @
      [rtac ctxt (Gset_map0 RS comp_eq_dest_lhs), rtac ctxt sym, rtac ctxt trans_o_apply,
      rtac ctxt trans_image_cong_o_apply, rtac ctxt trans_image_cong_o_apply,
-     rtac ctxt (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
+     rtac ctxt (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl]
+       RS trans),
      rtac ctxt @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac ctxt arg_cong_Union,
      rtac ctxt @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]},
      rtac ctxt @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
      [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac ctxt @{thm trans[OF image_insert]},
-        rtac ctxt @{thm arg_cong2[of _ _ _ _ insert]}, rtac ctxt @{thm ext}, rtac ctxt trans_o_apply,
-        rtac ctxt trans_image_cong_o_apply, rtac ctxt @{thm trans[OF image_image]},
-        rtac ctxt @{thm sym[OF trans[OF o_apply]]}, rtac ctxt @{thm image_cong[OF refl o_apply]}],
+        rtac ctxt @{thm arg_cong2[of _ _ _ _ insert]}, rtac ctxt @{thm ext},
+        rtac ctxt trans_o_apply, rtac ctxt trans_image_cong_o_apply,
+        rtac ctxt @{thm trans[OF image_image]}, rtac ctxt @{thm sym[OF trans[OF o_apply]]},
+        rtac ctxt @{thm image_cong[OF refl o_apply]}],
      rtac ctxt @{thm image_empty}]) 1;
 
 fun mk_comp_map_cong0_tac ctxt set'_eq_sets comp_set_alts map_cong0 map_cong0s =
@@ -96,9 +98,9 @@
           EVERY' [select_prem_tac ctxt n (dtac ctxt @{thm meta_spec}) (k + 1), etac ctxt meta_mp,
             rtac ctxt (equalityD2 RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans),
             rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union),
-            rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I}, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2},
-            rtac ctxt @{thm insertI1}, rtac ctxt (o_apply RS equalityD2 RS set_mp),
-            etac ctxt @{thm imageI}, assume_tac ctxt])
+            rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I},
+            REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1},
+            rtac ctxt (o_apply RS equalityD2 RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt])
           comp_set_alts))
       map_cong0s) 1)
   end;
@@ -220,14 +222,15 @@
 
 fun mk_permute_in_alt_tac ctxt src dest =
   (rtac ctxt @{thm Collect_cong} THEN'
-  mk_rotate_eq_tac ctxt (rtac ctxt refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
-    dest src) 1;
+  mk_rotate_eq_tac ctxt (rtac ctxt refl) trans @{thm conj_assoc} @{thm conj_commute}
+    @{thm conj_cong} dest src) 1;
 
 
 (* Miscellaneous *)
 
 fun mk_le_rel_OO_tac ctxt outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
-  EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
+  EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono ::
+    inner_le_rel_OOs)) 1;
 
 fun mk_simple_rel_OO_Grp_tac ctxt rel_OO_Grp in_alt_thm =
   rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -1300,10 +1300,12 @@
                 val funTs = map (fn T => bdT --> T) ranTs;
                 val ran_bnfT = mk_bnf_T ranTs Calpha;
                 val (revTs, Ts) = `rev (bd_bnfT :: funTs);
-                val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
-                val tinst = fold (fn T => fn t => HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs)
-                  (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
-                    map Bound (live - 1 downto 0)) $ Bound live));
+                val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT,
+                  Library.foldr1 HOLogic.mk_prodT Ts];
+                val tinst = fold (fn T => fn t =>
+                  HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs)
+                    (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
+                      map Bound (live - 1 downto 0)) $ Bound live));
                 val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
               in
                 Thm.instantiate' cTs cts @{thm surj_imp_ordLeq}
@@ -1420,7 +1422,8 @@
         val in_rel = Lazy.lazy mk_in_rel;
 
         fun mk_rel_flip () =
-          unfold_thms lthy @{thms conversep_iff} (Lazy.force rel_conversep RS @{thm predicate2_eqD});
+          unfold_thms lthy @{thms conversep_iff}
+            (Lazy.force rel_conversep RS @{thm predicate2_eqD});
 
         val rel_flip = Lazy.lazy mk_rel_flip;
 
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -97,18 +97,20 @@
 fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps =
   let
     val n = length set_maps;
-    val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans);
+    val rel_OO_Grps_tac =
+      if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans);
   in
     if null set_maps then
       unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
       rtac ctxt @{thm Grp_UNIV_idI[OF refl]} 1
     else
       EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I},
-        REPEAT_DETERM o
-          eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
-        hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
-        REPEAT_DETERM_N n o
-          EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
+        REPEAT_DETERM o eresolve_tac ctxt
+          [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+        hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp,
+          rtac ctxt map_cong0,
+        REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD},
+          etac ctxt @{thm set_mp}, assume_tac ctxt],
         rtac ctxt CollectI,
         CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
           rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
@@ -151,8 +153,9 @@
       unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
       TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
         resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
-        CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, assume_tac ctxt,
-        rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
+        CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI},
+        assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
+        resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
         CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
         REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
         dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -75,8 +75,8 @@
   val fp_sugar_of_global: theory -> string -> fp_sugar option
   val fp_sugars_of: Proof.context -> fp_sugar list
   val fp_sugars_of_global: theory -> fp_sugar list
-  val fp_sugars_interpretation: string ->
-    (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
+  val fp_sugars_interpretation: string -> (fp_sugar list -> local_theory -> local_theory) ->
+    theory -> theory
   val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
   val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
   val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
@@ -334,7 +334,7 @@
 );
 
 fun fp_sugar_of_generic context =
-  Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context)
+  Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context);
 
 fun fp_sugars_of_generic context =
   Symtab.fold (cons o transfer_fp_sugar (Context.theory_of context) o snd) (Data.get context) [];
@@ -1206,7 +1206,8 @@
   let
     val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
     val g_absTs = map range_type fun_Ts;
-    val g_Tsss = map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs);
+    val g_Tsss =
+      map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs);
     val g_Tssss = @{map 3} (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
       Cs ctr_Tsss' g_Tsss;
     val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss;
@@ -1312,7 +1313,8 @@
            ctor_rec_absTs reps fss xssss)))
   end;
 
-fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
+fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss
+    dtor_corec =
   let
     val nn = length fpTs;
     val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
@@ -1371,8 +1373,8 @@
 
     val rel_induct0_thm =
       Goal.prove_sorry lthy vars prems goal (fn {context = ctxt, prems} =>
-        mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts ctor_defss
-          ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
+        mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts
+          ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
       |> Thm.close_derivation;
   in
     (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
@@ -1713,8 +1715,8 @@
         val thm =
           Goal.prove_sorry lthy vars prems (HOLogic.mk_Trueprop concl)
             (fn {context = ctxt, prems} =>
-               mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts exhausts
-                 set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
+               mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts
+                 exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
           |> Thm.close_derivation;
 
         val case_names_attr =
@@ -1811,7 +1813,8 @@
              []
            else
              [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
-                Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]);
+                Library.foldr1 HOLogic.mk_conj
+                  (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]);
 
         fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
           Library.foldr1 HOLogic.mk_conj (flat (@{map 6} (mk_prem_ctr_concls rs' n)
@@ -2323,8 +2326,9 @@
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} =>
-             mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs) xsssss
-               rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
+             mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss)
+               (map (Thm.cterm_of ctxt) Rs) xsssss rec_defs xtor_co_rec_transfers pre_rel_defs
+               live_nesting_rel_eqs)
         |> Thm.close_derivation
         |> Conjunction.elim_balanced nn
       end;
@@ -2431,7 +2435,8 @@
         val rec_o_map_thmss = derive_rec_o_map_thmss lthy recs rec_defs;
 
         val simp_thmss =
-          @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
+          @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss
+            set_thmss;
 
         val common_notes =
           (if nn > 1 then
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -305,13 +305,15 @@
   end;
 
 fun solve_prem_prem_tac ctxt =
-  REPEAT o (eresolve_tac ctxt @{thms bexE rev_bexI} ORELSE' rtac ctxt @{thm rev_bexI[OF UNIV_I]} ORELSE'
-    hyp_subst_tac ctxt ORELSE' resolve_tac ctxt @{thms disjI1 disjI2}) THEN'
+  REPEAT o (eresolve_tac ctxt @{thms bexE rev_bexI} ORELSE'
+    rtac ctxt @{thm rev_bexI[OF UNIV_I]} ORELSE' hyp_subst_tac ctxt ORELSE'
+    resolve_tac ctxt @{thms disjI1 disjI2}) THEN'
   (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' rtac ctxt @{thm singletonI});
 
 fun mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
     pre_set_defs =
-  HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, etac ctxt meta_mp,
+  HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac ctxt nn (dtac ctxt meta_spec) kk,
+    etac ctxt meta_mp,
     SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @
       sumprod_thms_set)),
     solve_prem_prem_tac ctxt]) (rev kks)));
@@ -366,9 +368,10 @@
 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def fp_abs_inverse abs_inverse
     dtor_ctor exhaust ctr_defs discss selss =
   let val ks = 1 upto n in
-    EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, select_prem_tac ctxt nn (dtac ctxt meta_spec) kk,
-        dtac ctxt meta_spec, dtac ctxt meta_mp, assume_tac ctxt, rtac ctxt exhaust,
-        K (co_induct_inst_as_projs_tac ctxt 0), hyp_subst_tac ctxt] @
+    EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
+        select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, dtac ctxt meta_spec, dtac ctxt meta_mp,
+        assume_tac ctxt, rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 0),
+        hyp_subst_tac ctxt] @
       @{map 4} (fn k => fn ctr_def => fn discs => fn sels =>
         EVERY' ([rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @
           map2 (fn k' => fn discs' =>
@@ -435,8 +438,8 @@
         abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @
         @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False
           iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
-      REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN' (REPEAT_DETERM o rtac ctxt conjI) THEN'
-        (rtac ctxt refl ORELSE' assume_tac ctxt))))
+      REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN'
+        (REPEAT_DETERM o rtac ctxt conjI) THEN' (rtac ctxt refl ORELSE' assume_tac ctxt))))
     cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
       abs_inverses);
 
@@ -445,7 +448,8 @@
   rtac ctxt ctor_rel_induct 1 THEN EVERY (@{map 6} (fn cterm => fn exhaust => fn ctor_defs =>
       fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
         HEADGOAL (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
-          (rtac ctxt (infer_instantiate' ctxt (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
+          (rtac ctxt (infer_instantiate' ctxt (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2}
+              RS iffD2)
             THEN' assume_tac ctxt THEN' assume_tac ctxt THEN' TRY o resolve_tac ctxt assms))) THEN
         unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
           @{thms id_bnf_def vimage2p_def}) THEN
@@ -485,12 +489,14 @@
       (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
 
 fun mk_set_cases_tac ctxt ct assms exhaust sets =
-  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
+  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)
+    THEN_ALL_NEW hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt sets THEN
   REPEAT_DETERM (HEADGOAL
     (eresolve_tac ctxt @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
      hyp_subst_tac ctxt ORELSE'
-     SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o assume_tac ctxt)))));
+     SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o
+       assume_tac ctxt)))));
 
 fun mk_set_intros_tac ctxt sets =
   TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN
@@ -505,7 +511,8 @@
     val assms_tac =
       let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in
         fold (curry (op ORELSE')) (map (fn thm =>
-            funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt) (rtac ctxt thm)) assms')
+            funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt)
+              (rtac ctxt thm)) assms')
           (etac ctxt FalseE)
       end;
     val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
@@ -519,8 +526,8 @@
     unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
       @{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
         Un_empty_right empty_iff singleton_iff}) THEN
-    REPEAT (HEADGOAL (hyp_subst_tac ctxt ORELSE' eresolve_tac ctxt @{thms UN_E UnE singletonE} ORELSE'
-      assms_tac))
+    REPEAT (HEADGOAL (hyp_subst_tac ctxt ORELSE'
+      eresolve_tac ctxt @{thms UN_E UnE singletonE} ORELSE' assms_tac))
   end;
 
 end;
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -1009,8 +1009,8 @@
     |> map2 abs_curried_balanced arg_Tss
     |> (fn ts => Syntax.check_terms ctxt ts
       handle ERROR _ => nonprimitive_corec ctxt [])
-    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
-      bs mxs
+    |> @{map 3} (fn b => fn mx => fn t =>
+      ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) bs mxs
     |> rpair excludess'
   end;
 
@@ -1037,7 +1037,8 @@
         val prems = maps (s_not_conj o #prems) disc_eqns;
         val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE;
         val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE;
-        val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000; (* FIXME *)
+        val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt
+          |> the_default 100000; (* FIXME *)
 
         val extra_disc_eqn =
           {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no,
@@ -1307,7 +1308,8 @@
             Goal.prove_sorry lthy [] [] goal
               (fn {context = ctxt, prems = _} =>
                 mk_primcorec_sel_tac ctxt def_thms distincts split_sels split_sel_asms
-                fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss)
+                  fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m
+                  excludesss)
             |> Thm.close_derivation
             |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
             |> pair sel
@@ -1444,7 +1446,8 @@
                       Goal.prove_sorry lthy [] [] raw_goal
                         (fn {context = ctxt, prems = _} =>
                           mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms
-                            ms ctr_thms (if exhaustive_code then try the_single nchotomys else NONE))
+                            ms ctr_thms
+                            (if exhaustive_code then try the_single nchotomys else NONE))
                       |> Thm.close_derivation;
                   in
                     Goal.prove_sorry lthy [] [] goal
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -72,7 +72,8 @@
 fun mk_primcorec_assumption_tac ctxt discIs =
   SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
       not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
-    SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' etac ctxt conjE ORELSE'
+    SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
+    etac ctxt conjE ORELSE'
     eresolve_tac ctxt falseEs ORELSE'
     resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE'
     dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE'
@@ -137,7 +138,8 @@
     resolve_tac ctxt split_connectI ORELSE'
     Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
     Splitter.split_tac ctxt (split_if :: splits) ORELSE'
-    eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' assume_tac ctxt ORELSE'
+    eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
+    assume_tac ctxt ORELSE'
     etac ctxt notE THEN' assume_tac ctxt ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
          sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
@@ -148,7 +150,8 @@
 
 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
   HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
-    (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o assume_tac ctxt) THEN
+    (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN'
+    REPEAT_DETERM_N m o assume_tac ctxt) THEN
   unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl);
 
 fun inst_split_eq ctxt split =
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -458,7 +458,8 @@
     (recs, ctr_poss)
     |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
     |> Syntax.check_terms ctxt
-    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
+    |> @{map 3} (fn b => fn mx => fn t =>
+        ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
       bs mxs
   end;
 
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -40,7 +40,8 @@
   | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 =
     let
       val ((missing_arg_Ts, perm0_kks,
-            fp_sugars as {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _,
+            fp_sugars as {fp_nesting_bnfs,
+              fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _,
             (lfp_sugar_thms, _)), lthy) =
         nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
 
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -42,7 +42,8 @@
   Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps)))));
 
 fun register_size_global T_name size_name size_simps size_gen_o_maps =
-  Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps)))));
+  Context.theory_map
+    (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps)))));
 
 val size_of = Symtab.lookup o Data.get o Context.Proof;
 val size_of_global = Symtab.lookup o Data.get o Context.Theory;
@@ -70,8 +71,9 @@
 fun mk_size_neq ctxt cts exhaust sizes =
   HEADGOAL (rtac ctxt (infer_instantiate' ctxt (map SOME cts) exhaust)) THEN
   ALLGOALS (hyp_subst_tac ctxt) THEN
-  Ctr_Sugar_Tactics.unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN
-  ALLGOALS (REPEAT_DETERM o (rtac ctxt @{thm zero_less_Suc} ORELSE' rtac ctxt @{thm trans_less_add2}));
+  unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN
+  ALLGOALS (REPEAT_DETERM o (rtac ctxt @{thm zero_less_Suc} ORELSE'
+    rtac ctxt @{thm trans_less_add2}));
 
 fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
         fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs, ...} : fp_sugar) :: _)
@@ -236,7 +238,8 @@
         (Spec_Rules.retrieve lthy0 @{const size ('a)}
          |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
 
-      val nested_size_maps = map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
+      val nested_size_maps =
+        map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
       val all_inj_maps =
         @{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
         |> distinct Thm.eq_thm_prop;
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -50,8 +50,8 @@
   val ctr_sugars_of_global: theory -> ctr_sugar list
   val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
   val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
-  val ctr_sugar_interpretation: string ->
-    (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
+  val ctr_sugar_interpretation: string -> (ctr_sugar -> local_theory -> local_theory) -> theory ->
+    theory
   val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
   val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
   val register_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -54,7 +54,8 @@
 
 fun mk_nchotomy_tac ctxt n exhaust =
   HEADGOAL (rtac ctxt allI THEN' rtac ctxt exhaust THEN'
-    EVERY' (maps (fn k => [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
+    EVERY' (maps (fn k =>
+        [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
       (1 upto n)));
 
 fun mk_unique_disc_def_tac ctxt m uexhaust =
@@ -114,7 +115,8 @@
   else
     let val ks = 1 upto n in
       HEADGOAL (rtac ctxt uexhaust_disc THEN'
-        EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
+        EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' =>
+            fn uuncollapse =>
           EVERY' [rtac ctxt (uuncollapse RS trans) THEN'
             TRY o assume_tac ctxt, rtac ctxt sym, rtac ctxt vexhaust_disc,
             EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
@@ -124,13 +126,17 @@
                    (if m = 0 then
                       [rtac ctxt refl]
                     else
-                      [if n = 1 then K all_tac
-                       else EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp, assume_tac ctxt],
-                       REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE,
-                       asm_simp_tac (ss_only [] ctxt)])
+                      [if n = 1 then
+                         K all_tac
+                       else
+                         EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp,
+                           assume_tac ctxt],
+                         REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE,
+                         asm_simp_tac (ss_only [] ctxt)])
                  else
                    [dtac ctxt (the_single (if k = n then distinct_discs else distinct_discs')),
-                    etac ctxt (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
+                    etac ctxt (if k = n then @{thm iff_contradict(1)}
+                      else @{thm iff_contradict(2)}),
                     assume_tac ctxt, assume_tac ctxt]))
               ks distinct_discss distinct_discss' uncollapses)])
           ks ms distinct_discsss distinct_discsss' uncollapses))
@@ -152,8 +158,8 @@
     val ks = 1 upto n;
   in
     HEADGOAL (rtac ctxt (case_def' RS trans) THEN' rtac ctxt @{thm the_equality} THEN'
-      rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN' rtac ctxt refl THEN'
-      rtac ctxt refl THEN'
+      rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN'
+      rtac ctxt refl THEN' rtac ctxt refl THEN'
       EVERY' (map2 (fn k' => fn distincts =>
         (if k' < n then etac ctxt disjE else K all_tac) THEN'
         (if k' = k then mk_case_same_ctr_tac ctxt injects
@@ -182,7 +188,8 @@
        simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
          flat (nth distinctsss (k - 1))) ctxt)) k) THEN
     ALLGOALS (etac ctxt thin_rl THEN' rtac ctxt iffI THEN'
-      REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN' REPEAT_DETERM o etac ctxt conjE THEN'
+      REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN'
+      REPEAT_DETERM o etac ctxt conjE THEN'
       hyp_subst_tac ctxt THEN' assume_tac ctxt THEN'
       REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
       REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN'
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Dec 01 14:19:25 2015 +0000
@@ -66,11 +66,6 @@
 
 fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
 
-fun fp_sugar_only_type_ctr f fp_sugars =
-  (case filter (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugars of
-    [] => I
-  | fp_sugars' => f fp_sugars')
-
 (* relation constraints - bi_total & co. *)
 
 fun mk_relation_constraint name arg =
@@ -410,7 +405,7 @@
 
 fun transfer_fp_sugars_interpretation fp_sugar lthy =
   let
-    val lthy = pred_injects fp_sugar lthy
+    val lthy = lthy |> (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugar ? pred_injects fp_sugar
     val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar
   in
     lthy
@@ -419,7 +414,6 @@
   end
 
 val _ =
-  Theory.setup (fp_sugars_interpretation transfer_plugin
-    (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
+  Theory.setup (fp_sugars_interpretation transfer_plugin (fold transfer_fp_sugars_interpretation))
 
 end
diff -r d50b993b4fb9 -r 96d2c1b9a30a src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Tue Dec 01 14:09:10 2015 +0000
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Tue Dec 01 14:19:25 2015 +0000
@@ -1,5 +1,5 @@
 (*  Title:      HOL/ex/Higher_Order_Logic.thy
-    Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
+    Author:     Makarius
 *)
 
 section \<open>Foundations of HOL\<close>
@@ -9,12 +9,11 @@
 begin
 
 text \<open>
-  The following theory development demonstrates Higher-Order Logic
-  itself, represented directly within the Pure framework of Isabelle.
-  The ``HOL'' logic given here is essentially that of Gordon
-  @{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts
-  in a slightly more conventional manner oriented towards plain
-  Natural Deduction.
+  The following theory development demonstrates Higher-Order Logic itself,
+  represented directly within the Pure framework of Isabelle. The ``HOL''
+  logic given here is essentially that of Gordon @{cite "Gordon:1985:HOL"},
+  although we prefer to present basic concepts in a slightly more conventional
+  manner oriented towards plain Natural Deduction.
 \<close>
 
 
@@ -30,35 +29,31 @@
 
 subsubsection \<open>Basic logical connectives\<close>
 
-judgment Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
+judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
 
-axiomatization
-  imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25) and
-  All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
-where
-  impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
-  impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
-  allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
-  allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
+axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
+  where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
+    and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
+
+axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
+  where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
+    and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
 
 
 subsubsection \<open>Extensional equality\<close>
 
-axiomatization
-  equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
-where
-  refl [intro]: "x = x" and
-  subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
+axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "=" 50)
+  where refl [intro]: "x = x"
+    and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
 
-axiomatization where
-  ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and
-  iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
+axiomatization
+  where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
+    and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
 
-theorem sym [sym]: "x = y \<Longrightarrow> y = x"
-proof -
-  assume "x = y"
-  then show "y = x" by (rule subst) (rule refl)
-qed
+theorem sym [sym]:
+  assumes "x = y"
+  shows "y = x"
+  using assms by (rule subst) (rule refl)
 
 lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
   by (rule subst) (rule sym)
@@ -80,173 +75,187 @@
 
 definition false :: o  ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
 
+theorem falseE [elim]:
+  assumes "\<bottom>"
+  shows A
+proof -
+  from \<open>\<bottom>\<close> have "\<forall>A. A" unfolding false_def .
+  then show A ..
+qed
+
+
 definition true :: o  ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
 
+theorem trueI [intro]: \<top>
+  unfolding true_def ..
+
+
 definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
   where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
 
-definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
-  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-
-definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
-  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-
-definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
-  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-
 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
   where "x \<noteq> y \<equiv> \<not> (x = y)"
 
-theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
-proof (unfold false_def)
-  assume "\<forall>A. A"
-  then show A ..
-qed
-
-theorem trueI [intro]: \<top>
-proof (unfold true_def)
-  show "\<bottom> \<longrightarrow> \<bottom>" ..
-qed
+theorem notI [intro]:
+  assumes "A \<Longrightarrow> \<bottom>"
+  shows "\<not> A"
+  using assms unfolding not_def ..
 
-theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
-proof (unfold not_def)
-  assume "A \<Longrightarrow> \<bottom>"
-  then show "A \<longrightarrow> \<bottom>" ..
-qed
-
-theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
-proof (unfold not_def)
-  assume "A \<longrightarrow> \<bottom>" and A
-  then have \<bottom> ..
+theorem notE [elim]:
+  assumes "\<not> A" and A
+  shows B
+proof -
+  from \<open>\<not> A\<close> have "A \<longrightarrow> \<bottom>" unfolding not_def .
+  from this and \<open>A\<close> have "\<bottom>" ..
   then show B ..
 qed
 
 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   by (rule notE)
 
-lemmas contradiction = notE notE'  -- \<open>proof by contradiction in any order\<close>
+lemmas contradiction = notE notE'  \<comment> \<open>proof by contradiction in any order\<close>
+
+
+definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
+  where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
 
-theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
-proof (unfold conj_def)
-  assume A and B
-  show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
+theorem conjI [intro]:
+  assumes A and B
+  shows "A \<and> B"
+  unfolding conj_def
+proof
+  fix C
+  show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   proof
-    fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-    proof
-      assume "A \<longrightarrow> B \<longrightarrow> C"
-      also note \<open>A\<close>
-      also note \<open>B\<close>
-      finally show C .
-    qed
+    assume "A \<longrightarrow> B \<longrightarrow> C"
+    also note \<open>A\<close>
+    also note \<open>B\<close>
+    finally show C .
   qed
 qed
 
-theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
-proof (unfold conj_def)
-  assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
-  assume "A \<Longrightarrow> B \<Longrightarrow> C"
-  moreover {
-    from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
+theorem conjE [elim]:
+  assumes "A \<and> B"
+  obtains A and B
+proof
+  from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
+    unfolding conj_def ..
+  show A
+  proof -
+    note * [of A]
     also have "A \<longrightarrow> B \<longrightarrow> A"
     proof
       assume A
       then show "B \<longrightarrow> A" ..
     qed
-    finally have A .
-  } moreover {
-    from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
+    finally show ?thesis .
+  qed
+  show B
+  proof -
+    note * [of B]
     also have "A \<longrightarrow> B \<longrightarrow> B"
     proof
       show "B \<longrightarrow> B" ..
     qed
-    finally have B .
-  } ultimately show C .
-qed
-
-theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
-proof (unfold disj_def)
-  assume A
-  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-  proof
-    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-    proof
-      assume "A \<longrightarrow> C"
-      also note \<open>A\<close>
-      finally have C .
-      then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
-    qed
+    finally show ?thesis .
   qed
 qed
 
-theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
-proof (unfold disj_def)
-  assume B
-  show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+
+definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
+  where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+
+theorem disjI1 [intro]:
+  assumes A
+  shows "A \<or> B"
+  unfolding disj_def
+proof
+  fix C
+  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   proof
-    fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+    assume "A \<longrightarrow> C"
+    from this and \<open>A\<close> have C ..
+    then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
+  qed
+qed
+
+theorem disjI2 [intro]:
+  assumes B
+  shows "A \<or> B"
+  unfolding disj_def
+proof
+  fix C
+  show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
+  proof
+    show "(B \<longrightarrow> C) \<longrightarrow> C"
     proof
-      show "(B \<longrightarrow> C) \<longrightarrow> C"
-      proof
-        assume "B \<longrightarrow> C"
-        also note \<open>B\<close>
-        finally show C .
-      qed
+      assume "B \<longrightarrow> C"
+      from this and \<open>B\<close> show C ..
     qed
   qed
 qed
 
-theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
-proof (unfold disj_def)
-  assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
-  assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
-  from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
-  also have "A \<longrightarrow> C"
+theorem disjE [elim]:
+  assumes "A \<or> B"
+  obtains (a) A | (b) B
+proof -
+  from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
+    unfolding disj_def ..
+  also have "A \<longrightarrow> thesis"
   proof
     assume A
-    then show C by (rule r1)
+    then show thesis by (rule a)
   qed
-  also have "B \<longrightarrow> C"
+  also have "B \<longrightarrow> thesis"
   proof
     assume B
-    then show C by (rule r2)
+    then show thesis by (rule b)
   qed
-  finally show C .
+  finally show thesis .
 qed
 
+
+definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
+  where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+
 theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
-proof (unfold Ex_def)
+  unfolding Ex_def
+proof
+  fix C
   assume "P a"
-  show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
+  show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   proof
-    fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-    proof
-      assume "\<forall>x. P x \<longrightarrow> C"
-      then have "P a \<longrightarrow> C" ..
-      also note \<open>P a\<close>
-      finally show C .
-    qed
+    assume "\<forall>x. P x \<longrightarrow> C"
+    then have "P a \<longrightarrow> C" ..
+    from this and \<open>P a\<close> show C ..
   qed
 qed
 
-theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
-proof (unfold Ex_def)
-  assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
-  assume r: "\<And>x. P x \<Longrightarrow> C"
-  from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
-  also have "\<forall>x. P x \<longrightarrow> C"
+theorem exE [elim]:
+  assumes "\<exists>x. P x"
+  obtains (that) x where "P x"
+proof -
+  from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
+    unfolding Ex_def ..
+  also have "\<forall>x. P x \<longrightarrow> thesis"
   proof
-    fix x show "P x \<longrightarrow> C"
+    fix x
+    show "P x \<longrightarrow> thesis"
     proof
       assume "P x"
-      then show C by (rule r)
+      then show thesis by (rule that)
     qed
   qed
-  finally show C .
+  finally show thesis .
 qed
 
 
 subsection \<open>Classical logic\<close>
 
+text \<open>
+  The subsequent rules of classical reasoning are all equivalent.
+\<close>
+
 locale classical =
   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
 
@@ -265,14 +274,12 @@
   qed
 qed
 
-theorem (in classical) double_negation: "\<not> \<not> A \<Longrightarrow> A"
-proof -
-  assume "\<not> \<not> A"
-  show A
-  proof (rule classical)
-    assume "\<not> A"
-    with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
-  qed
+theorem (in classical) double_negation:
+  assumes "\<not> \<not> A"
+  shows A
+proof (rule classical)
+  assume "\<not> A"
+  with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
 qed
 
 theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
@@ -290,27 +297,30 @@
   qed
 qed
 
-theorem (in classical) classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
-proof -
-  assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
-  from tertium_non_datur show C
-  proof
+theorem (in classical) classical_cases:
+  obtains A | "\<not> A"
+  using tertium_non_datur
+proof
+  assume A
+  then show thesis ..
+next
+  assume "\<not> A"
+  then show thesis ..
+qed
+
+lemma
+  assumes classical_cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
+  shows "PROP classical"
+proof
+  fix A
+  assume *: "\<not> A \<Longrightarrow> A"
+  show A
+  proof (rule classical_cases)
     assume A
-    then show ?thesis by (rule r1)
+    then show A .
   next
     assume "\<not> A"
-    then show ?thesis by (rule r2)
-  qed
-qed
-
-lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
-proof -
-  assume r: "\<not> A \<Longrightarrow> A"
-  show A
-  proof (rule classical_cases)
-    assume A then show A .
-  next
-    assume "\<not> A" then show A by (rule r)
+    then show A by (rule *)
   qed
 qed