diff -r 27f3c10b0b50 -r 4cf66f21b764 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Set.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -10,8 +10,8 @@
 
 typedecl 'a set
 
-axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" -- "comprehension"
-  and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" -- "membership"
+axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" \<comment> "comprehension"
+  and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> "membership"
 where
   mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
   and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
@@ -21,7 +21,7 @@
   member  ("(_/ : _)" [51, 51] 50)
 
 abbreviation not_member where
-  "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
+  "not_member x A \<equiv> ~ (x : A)" \<comment> "non-membership"
 
 notation
   not_member  ("op ~:") and
@@ -58,8 +58,8 @@
   by simp
 
 text \<open>
-Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
-to the front (and similarly for @{text "t=x"}):
+Simproc for pulling \<open>x=t\<close> in \<open>{x. \<dots> & x=t & \<dots>}\<close>
+to the front (and similarly for \<open>t=x\<close>):
 \<close>
 
 simproc_setup defined_Collect ("{x. P x & Q x}") = \<open>
@@ -176,10 +176,10 @@
   supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
 
 definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   -- "bounded universal quantifiers"
+  "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   \<comment> "bounded universal quantifiers"
 
 definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   -- "bounded existential quantifiers"
+  "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   \<comment> "bounded existential quantifiers"
 
 syntax
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
@@ -267,9 +267,8 @@
 
 
 text \<open>
-  \medskip Translate between @{text "{e | x1...xn. P}"} and @{text
-  "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is
-  only translated if @{text "[0..n] subset bvs(e)"}.
+  \medskip Translate between \<open>{e | x1...xn. P}\<close> and \<open>{u. EX x1..xn. u = e & P}\<close>; \<open>{y. EX x1..xn. y = e & P}\<close> is
+  only translated if \<open>[0..n] subset bvs(e)\<close>.
 \<close>
 
 syntax
@@ -295,7 +294,7 @@
 print_translation \<open>
  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
   Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
-\<close> -- \<open>to avoid eta-contraction of body\<close>
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 print_translation \<open>
 let
@@ -383,12 +382,12 @@
   by (unfold Ball_def) blast
 
 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
-  -- \<open>Normally the best argument order: @{prop "P x"} constrains the
+  \<comment> \<open>Normally the best argument order: @{prop "P x"} constrains the
     choice of @{prop "x:A"}.\<close>
   by (unfold Bex_def) blast
 
 lemma rev_bexI [intro?]: "x:A ==> P x ==> EX x:A. P x"
-  -- \<open>The best argument order when there is only one @{prop "x:A"}.\<close>
+  \<comment> \<open>The best argument order when there is only one @{prop "x:A"}.\<close>
   by (unfold Bex_def) blast
 
 lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"
@@ -398,11 +397,11 @@
   by (unfold Bex_def) blast
 
 lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"
-  -- \<open>Trival rewrite rule.\<close>
+  \<comment> \<open>Trival rewrite rule.\<close>
   by (simp add: Ball_def)
 
 lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"
-  -- \<open>Dual form for existentials.\<close>
+  \<comment> \<open>Dual form for existentials.\<close>
   by (simp add: Bex_def)
 
 lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"
@@ -465,18 +464,18 @@
   by (simp add: less_eq_set_def le_fun_def)
 
 text \<open>
-  \medskip Map the type @{text "'a set => anything"} to just @{typ
+  \medskip Map the type \<open>'a set => anything\<close> to just @{typ
   'a}; for overloading constants whose first argument has type @{typ
   "'a set"}.
 \<close>
 
 lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
   by (simp add: less_eq_set_def le_fun_def)
-  -- \<open>Rule in Modus Ponens style.\<close>
+  \<comment> \<open>Rule in Modus Ponens style.\<close>
 
 lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
-  -- \<open>The same, with reversed premises for use with @{text erule} --
-      cf @{text rev_mp}.\<close>
+  \<comment> \<open>The same, with reversed premises for use with \<open>erule\<close> --
+      cf \<open>rev_mp\<close>.\<close>
   by (rule subsetD)
 
 text \<open>
@@ -484,7 +483,7 @@
 \<close>
 
 lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
-  -- \<open>Classical elimination rule.\<close>
+  \<comment> \<open>Classical elimination rule.\<close>
   by (auto simp add: less_eq_set_def le_fun_def)
 
 lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
@@ -518,7 +517,7 @@
 subsubsection \<open>Equality\<close>
 
 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
-  -- \<open>Anti-symmetry of the subset relation.\<close>
+  \<comment> \<open>Anti-symmetry of the subset relation.\<close>
   by (iprover intro: set_eqI subsetD)
 
 text \<open>
@@ -533,8 +532,7 @@
   by simp
 
 text \<open>
-  \medskip Be careful when adding this to the claset as @{text
-  subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
+  \medskip Be careful when adding this to the claset as \<open>subset_empty\<close> is in the simpset: @{prop "A = {}"} goes to @{prop "{}
   \<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}!
 \<close>
 
@@ -565,14 +563,14 @@
   by simp
 
 lemma empty_subsetI [iff]: "{} \<subseteq> A"
-    -- \<open>One effect is to delete the ASSUMPTION @{prop "{} <= A"}\<close>
+    \<comment> \<open>One effect is to delete the ASSUMPTION @{prop "{} <= A"}\<close>
   by blast
 
 lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
   by blast
 
 lemma equals0D: "A = {} ==> a \<notin> A"
-    -- \<open>Use for reasoning about disjointness: @{text "A Int B = {}"}\<close>
+    \<comment> \<open>Use for reasoning about disjointness: \<open>A Int B = {}\<close>\<close>
   by blast
 
 lemma ball_empty [simp]: "Ball {} P = True"
@@ -594,7 +592,7 @@
 lemma UNIV_I [simp]: "x : UNIV"
   by (simp add: UNIV_def)
 
-declare UNIV_I [intro]  -- \<open>unsafe makes it less likely to cause problems\<close>
+declare UNIV_I [intro]  \<comment> \<open>unsafe makes it less likely to cause problems\<close>
 
 lemma UNIV_witness [intro?]: "EX x. x : UNIV"
   by simp
@@ -603,7 +601,7 @@
   by (fact top_greatest) (* already simp *)
 
 text \<open>
-  \medskip Eta-contracting these two rules (to remove @{text P})
+  \medskip Eta-contracting these two rules (to remove \<open>P\<close>)
   causes them to be ignored because of their interaction with
   congruence rules.
 \<close>
@@ -777,7 +775,7 @@
   by (unfold insert_def) blast
 
 lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
-  -- \<open>Classical introduction rule.\<close>
+  \<comment> \<open>Classical introduction rule.\<close>
   by auto
 
 lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
@@ -821,7 +819,7 @@
 subsubsection \<open>Singletons, using insert\<close>
 
 lemma singletonI [intro!]: "a : {a}"
-    -- \<open>Redundant? But unlike @{text insertCI}, it proves the subgoal immediately!\<close>
+    \<comment> \<open>Redundant? But unlike \<open>insertCI\<close>, it proves the subgoal immediately!\<close>
   by (rule insertI1)
 
 lemma singletonD [dest!]: "b : {a} ==> b = a"
@@ -887,12 +885,12 @@
 
 lemma rev_image_eqI:
   "x \<in> A \<Longrightarrow> b = f x \<Longrightarrow> b \<in> f ` A"
-  -- \<open>This version's more effective when we already have the
+  \<comment> \<open>This version's more effective when we already have the
     required @{term x}.\<close>
   by (rule image_eqI)
 
 lemma imageE [elim!]:
-  assumes "b \<in> (\<lambda>x. f x) ` A" -- \<open>The eta-expansion gives variable-name preservation.\<close>
+  assumes "b \<in> (\<lambda>x. f x) ` A" \<comment> \<open>The eta-expansion gives variable-name preservation.\<close>
   obtains x where "b = f x" and "x \<in> A"
   using assms by (unfold image_def) blast
 
@@ -910,13 +908,13 @@
 
 lemma image_subsetI:
   "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` A \<subseteq> B"
-  -- \<open>Replaces the three steps @{text subsetI}, @{text imageE},
-    @{text hypsubst}, but breaks too many existing proofs.\<close>
+  \<comment> \<open>Replaces the three steps \<open>subsetI\<close>, \<open>imageE\<close>,
+    \<open>hypsubst\<close>, but breaks too many existing proofs.\<close>
   by blast
 
 lemma image_subset_iff:
   "f ` A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> B)"
-  -- \<open>This rewrite rule would confuse users if made default.\<close>
+  \<comment> \<open>This rewrite rule would confuse users if made default.\<close>
   by blast
 
 lemma subset_imageE:
@@ -970,7 +968,7 @@
 
 lemma image_Collect:
   "f ` {x. P x} = {f x | x. P x}"
-  -- \<open>NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
+  \<comment> \<open>NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
       with its implicit quantifier and conjunction.  Also image enjoys better
       equational properties than does the RHS.\<close>
   by blast
@@ -1011,7 +1009,7 @@
 \<close>
 
 abbreviation range :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set"
-where -- "of function"
+where \<comment> "of function"
   "range f \<equiv> f ` UNIV"
 
 lemma range_eqI:
@@ -1035,9 +1033,9 @@
   by auto
 
 
-subsubsection \<open>Some rules with @{text "if"}\<close>
-
-text\<open>Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}.\<close>
+subsubsection \<open>Some rules with \<open>if\<close>\<close>
+
+text\<open>Elimination of \<open>{x. \<dots> & x=t & \<dots>}\<close>.\<close>
 
 lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
   by auto
@@ -1046,8 +1044,7 @@
   by auto
 
 text \<open>
-  Rewrite rules for boolean case-splitting: faster than @{text
-  "split_if [split]"}.
+  Rewrite rules for boolean case-splitting: faster than \<open>split_if [split]\<close>.
 \<close>
 
 lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
@@ -1057,8 +1054,7 @@
   by (rule split_if)
 
 text \<open>
-  Split ifs on either side of the membership relation.  Not for @{text
-  "[simp]"} -- can cause goals to blow up!
+  Split ifs on either side of the membership relation.  Not for \<open>[simp]\<close> -- can cause goals to blow up!
 \<close>
 
 lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
@@ -1139,7 +1135,7 @@
 
 subsubsection \<open>Derived rules involving subsets.\<close>
 
-text \<open>@{text insert}.\<close>
+text \<open>\<open>insert\<close>.\<close>
 
 lemma subset_insertI: "B \<subseteq> insert a B"
   by (rule subsetI) (erule insertI2)
@@ -1186,10 +1182,10 @@
 
 subsubsection \<open>Equalities involving union, intersection, inclusion, etc.\<close>
 
-text \<open>@{text "{}"}.\<close>
+text \<open>\<open>{}\<close>.\<close>
 
 lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
-  -- \<open>supersedes @{text "Collect_False_empty"}\<close>
+  \<comment> \<open>supersedes \<open>Collect_False_empty\<close>\<close>
   by auto
 
 lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
@@ -1220,10 +1216,10 @@
   by blast
 
 
-text \<open>\medskip @{text insert}.\<close>
+text \<open>\medskip \<open>insert\<close>.\<close>
 
 lemma insert_is_Un: "insert a A = {a} Un A"
-  -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"}\<close>
+  \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} == insert a {}\<close>\<close>
   by blast
 
 lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
@@ -1233,8 +1229,8 @@
 declare empty_not_insert [simp]
 
 lemma insert_absorb: "a \<in> A ==> insert a A = A"
-  -- \<open>@{text "[simp]"} causes recursive calls when there are nested inserts\<close>
-  -- \<open>with \emph{quadratic} running time\<close>
+  \<comment> \<open>\<open>[simp]\<close> causes recursive calls when there are nested inserts\<close>
+  \<comment> \<open>with \emph{quadratic} running time\<close>
   by blast
 
 lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
@@ -1247,7 +1243,7 @@
   by blast
 
 lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
-  -- \<open>use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding\<close>
+  \<comment> \<open>use new \<open>B\<close> rather than \<open>A - {a}\<close> to avoid infinite unfolding\<close>
   apply (rule_tac x = "A - {a}" in exI, blast)
   done
 
@@ -1268,7 +1264,7 @@
   by auto
 
 
-text \<open>\medskip @{text Int}\<close>
+text \<open>\medskip \<open>Int\<close>\<close>
 
 lemma Int_absorb: "A \<inter> A = A"
   by (fact inf_idem) (* already simp *)
@@ -1286,7 +1282,7 @@
   by (fact inf_assoc)
 
 lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
-  -- \<open>Intersection is an AC-operator\<close>
+  \<comment> \<open>Intersection is an AC-operator\<close>
 
 lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
   by (fact inf_absorb2)
@@ -1328,7 +1324,7 @@
   by blast
 
 
-text \<open>\medskip @{text Un}.\<close>
+text \<open>\medskip \<open>Un\<close>.\<close>
 
 lemma Un_absorb: "A \<union> A = A"
   by (fact sup_idem) (* already simp *)
@@ -1346,7 +1342,7 @@
   by (fact sup_assoc)
 
 lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
-  -- \<open>Union is an AC-operator\<close>
+  \<comment> \<open>Union is an AC-operator\<close>
 
 lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
   by (fact sup_absorb2)
@@ -1449,7 +1445,7 @@
   by blast
 
 lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
-  -- \<open>Halmos, Naive Set Theory, page 16.\<close>
+  \<comment> \<open>Halmos, Naive Set Theory, page 16.\<close>
   by blast
 
 lemma Compl_UNIV_eq: "-UNIV = {}"
@@ -1470,7 +1466,7 @@
 text \<open>\medskip Bounded quantifiers.
 
   The following are not added to the default simpset because
-  (a) they duplicate the body and (b) there are no similar rules for @{text Int}.\<close>
+  (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close>
 
 lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
   by blast
@@ -1509,11 +1505,11 @@
   by blast
 
 lemma Diff_insert: "A - insert a B = A - B - {a}"
-  -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"}\<close>
+  \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} == insert a 0\<close>\<close>
   by blast
 
 lemma Diff_insert2: "A - insert a B = A - {a} - B"
-  -- \<open>NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"}\<close>
+  \<comment> \<open>NOT SUITABLE FOR REWRITING since \<open>{a} == insert a 0\<close>\<close>
   by blast
 
 lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
@@ -1591,7 +1587,7 @@
 lemma UNIV_bool: "UNIV = {False, True}"
   by (auto intro: bool_induct)
 
-text \<open>\medskip @{text Pow}\<close>
+text \<open>\medskip \<open>Pow\<close>\<close>
 
 lemma Pow_empty [simp]: "Pow {} = {{}}"
   by (auto simp add: Pow_def)
@@ -1764,7 +1760,7 @@
   by blast
 
 lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
-  -- \<open>NOT suitable for rewriting because of the recurrence of @{term "{a}"}.\<close>
+  \<comment> \<open>NOT suitable for rewriting because of the recurrence of @{term "{a}"}.\<close>
   by blast
 
 lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
@@ -1774,7 +1770,7 @@
   by blast
 
 lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
-  -- \<open>monotonicity\<close>
+  \<comment> \<open>monotonicity\<close>
   by blast
 
 lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
@@ -1831,7 +1827,7 @@
 lemma Least_mono:
   "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
     ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
-    -- \<open>Courtesy of Stephan Merz\<close>
+    \<comment> \<open>Courtesy of Stephan Merz\<close>
   apply clarify
   apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
   apply (rule LeastI2_order)