--- a/src/Doc/Tutorial/Sets/Examples.thy Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Sets/Examples.thy Fri Jan 12 14:08:53 2018 +0100
@@ -2,14 +2,14 @@
declare [[eta_contract = false]]
-text{*membership, intersection *}
-text{*difference and empty set*}
-text{*complement, union and universal set*}
+text\<open>membership, intersection\<close>
+text\<open>difference and empty set\<close>
+text\<open>complement, union and universal set\<close>
lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
by blast
-text{*
+text\<open>
@{thm[display] IntI[no_vars]}
\rulename{IntI}
@@ -18,60 +18,60 @@
@{thm[display] IntD2[no_vars]}
\rulename{IntD2}
-*}
+\<close>
lemma "(x \<in> -A) = (x \<notin> A)"
by blast
-text{*
+text\<open>
@{thm[display] Compl_iff[no_vars]}
\rulename{Compl_iff}
-*}
+\<close>
lemma "- (A \<union> B) = -A \<inter> -B"
by blast
-text{*
+text\<open>
@{thm[display] Compl_Un[no_vars]}
\rulename{Compl_Un}
-*}
+\<close>
lemma "A-A = {}"
by blast
-text{*
+text\<open>
@{thm[display] Diff_disjoint[no_vars]}
\rulename{Diff_disjoint}
-*}
+\<close>
lemma "A \<union> -A = UNIV"
by blast
-text{*
+text\<open>
@{thm[display] Compl_partition[no_vars]}
\rulename{Compl_partition}
-*}
+\<close>
-text{*subset relation*}
+text\<open>subset relation\<close>
-text{*
+text\<open>
@{thm[display] subsetI[no_vars]}
\rulename{subsetI}
@{thm[display] subsetD[no_vars]}
\rulename{subsetD}
-*}
+\<close>
lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
by blast
-text{*
+text\<open>
@{thm[display] Un_subset_iff[no_vars]}
\rulename{Un_subset_iff}
-*}
+\<close>
lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
by blast
@@ -79,19 +79,19 @@
lemma "(A <= -B) = (B <= -A)"
oops
-text{*ASCII version: blast fails because of overloading because
- it doesn't have to be sets*}
+text\<open>ASCII version: blast fails because of overloading because
+ it doesn't have to be sets\<close>
lemma "((A:: 'a set) <= -B) = (B <= -A)"
by blast
-text{*A type constraint lets it work*}
+text\<open>A type constraint lets it work\<close>
-text{*An issue here: how do we discuss the distinction between ASCII and
-symbol notation? Here the latter disambiguates.*}
+text\<open>An issue here: how do we discuss the distinction between ASCII and
+symbol notation? Here the latter disambiguates.\<close>
-text{*
+text\<open>
set extensionality
@{thm[display] set_eqI[no_vars]}
@@ -102,19 +102,19 @@
@{thm[display] equalityE[no_vars]}
\rulename{equalityE}
-*}
+\<close>
-text{*finite sets: insertion and membership relation*}
-text{*finite set notation*}
+text\<open>finite sets: insertion and membership relation\<close>
+text\<open>finite set notation\<close>
lemma "insert x A = {x} \<union> A"
by blast
-text{*
+text\<open>
@{thm[display] insert_is_Un[no_vars]}
\rulename{insert_is_Un}
-*}
+\<close>
lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
by blast
@@ -122,31 +122,31 @@
lemma "{a,b} \<inter> {b,c} = {b}"
apply auto
oops
-text{*fails because it isn't valid*}
+text\<open>fails because it isn't valid\<close>
lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
apply simp
by blast
-text{*or just force or auto. blast alone can't handle the if-then-else*}
+text\<open>or just force or auto. blast alone can't handle the if-then-else\<close>
-text{*next: some comprehension examples*}
+text\<open>next: some comprehension examples\<close>
lemma "(a \<in> {z. P z}) = P a"
by blast
-text{*
+text\<open>
@{thm[display] mem_Collect_eq[no_vars]}
\rulename{mem_Collect_eq}
-*}
+\<close>
lemma "{x. x \<in> A} = A"
by blast
-text{*
+text\<open>
@{thm[display] Collect_mem_eq[no_vars]}
\rulename{Collect_mem_eq}
-*}
+\<close>
lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
by blast
@@ -161,50 +161,50 @@
{z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"
by (rule refl)
-text{*binders*}
+text\<open>binders\<close>
-text{*bounded quantifiers*}
+text\<open>bounded quantifiers\<close>
lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
by blast
-text{*
+text\<open>
@{thm[display] bexI[no_vars]}
\rulename{bexI}
-*}
+\<close>
-text{*
+text\<open>
@{thm[display] bexE[no_vars]}
\rulename{bexE}
-*}
+\<close>
lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
by blast
-text{*
+text\<open>
@{thm[display] ballI[no_vars]}
\rulename{ballI}
-*}
+\<close>
-text{*
+text\<open>
@{thm[display] bspec[no_vars]}
\rulename{bspec}
-*}
+\<close>
-text{*indexed unions and variations*}
+text\<open>indexed unions and variations\<close>
lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
by blast
-text{*
+text\<open>
@{thm[display] UN_iff[no_vars]}
\rulename{UN_iff}
-*}
+\<close>
-text{*
+text\<open>
@{thm[display] Union_iff[no_vars]}
\rulename{Union_iff}
-*}
+\<close>
lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
by blast
@@ -212,35 +212,35 @@
lemma "\<Union>S = (\<Union>x\<in>S. x)"
by blast
-text{*
+text\<open>
@{thm[display] UN_I[no_vars]}
\rulename{UN_I}
-*}
+\<close>
-text{*
+text\<open>
@{thm[display] UN_E[no_vars]}
\rulename{UN_E}
-*}
+\<close>
-text{*indexed intersections*}
+text\<open>indexed intersections\<close>
lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
by blast
-text{*
+text\<open>
@{thm[display] INT_iff[no_vars]}
\rulename{INT_iff}
-*}
+\<close>
-text{*
+text\<open>
@{thm[display] Inter_iff[no_vars]}
\rulename{Inter_iff}
-*}
+\<close>
-text{*mention also card, Pow, etc.*}
+text\<open>mention also card, Pow, etc.\<close>
-text{*
+text\<open>
@{thm[display] card_Un_Int[no_vars]}
\rulename{card_Un_Int}
@@ -249,6 +249,6 @@
@{thm[display] n_subsets[no_vars]}
\rulename{n_subsets}
-*}
+\<close>
end