src/Doc/Tutorial/Sets/Functions.thy

--- a/src/Doc/Tutorial/Sets/Functions.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Sets/Functions.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -1,7 +1,7 @@
 theory Functions imports Main begin
 
 
-text{*
+text\<open>
 @{thm[display] id_def[no_vars]}
 \rulename{id_def}
 
@@ -10,18 +10,18 @@
 
 @{thm[display] o_assoc[no_vars]}
 \rulename{o_assoc}
-*}
+\<close>
 
-text{*
+text\<open>
 @{thm[display] fun_upd_apply[no_vars]}
 \rulename{fun_upd_apply}
 
 @{thm[display] fun_upd_upd[no_vars]}
 \rulename{fun_upd_upd}
-*}
+\<close>
 
 
-text{*
+text\<open>
 definitions of injective, surjective, bijective
 
 @{thm[display] inj_on_def[no_vars]}
@@ -32,15 +32,15 @@
 
 @{thm[display] bij_def[no_vars]}
 \rulename{bij_def}
-*}
+\<close>
 
 
 
-text{*
+text\<open>
 possibly interesting theorems about inv
-*}
+\<close>
 
-text{*
+text\<open>
 @{thm[display] inv_f_f[no_vars]}
 \rulename{inv_f_f}
 
@@ -61,9 +61,9 @@
 
 @{thm[display] o_inv_distrib[no_vars]}
 \rulename{o_inv_distrib}
-*}
+\<close>
 
-text{*
+text\<open>
 small sample proof
 
 @{thm[display] ext[no_vars]}
@@ -71,35 +71,35 @@
 
 @{thm[display] fun_eq_iff[no_vars]}
 \rulename{fun_eq_iff}
-*}
+\<close>
 
 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"
   apply (simp add: fun_eq_iff inj_on_def)
   apply (auto)
   done
 
-text{*
+text\<open>
 \begin{isabelle}
 inj\ f\ \isasymLongrightarrow \ (f\ \isasymcirc \ g\ =\ f\ \isasymcirc \ h)\ =\ (g\ =\ h)\isanewline
 \ 1.\ \isasymforall x\ y.\ f\ x\ =\ f\ y\ \isasymlongrightarrow \ x\ =\ y\ \isasymLongrightarrow \isanewline
 \ \ \ \ (\isasymforall x.\ f\ (g\ x)\ =\ f\ (h\ x))\ =\ (\isasymforall x.\ g\ x\ =\ h\ x)
 \end{isabelle}
-*}
+\<close>
  
 
-text{*image, inverse image*}
+text\<open>image, inverse image\<close>
 
-text{*
+text\<open>
 @{thm[display] image_def[no_vars]}
 \rulename{image_def}
-*}
+\<close>
 
-text{*
+text\<open>
 @{thm[display] image_Un[no_vars]}
 \rulename{image_Un}
-*}
+\<close>
 
-text{*
+text\<open>
 @{thm[display] image_comp[no_vars]}
 \rulename{image_comp}
 
@@ -108,12 +108,12 @@
 
 @{thm[display] bij_image_Compl_eq[no_vars]}
 \rulename{bij_image_Compl_eq}
-*}
+\<close>
 
 
-text{*
+text\<open>
 illustrates Union as well as image
-*}
+\<close>
 
 lemma "f`A \<union> g`A = (\<Union>x\<in>A. {f x, g x})"
 by blast
@@ -121,23 +121,23 @@
 lemma "f ` {(x,y). P x y} = {f(x,y) | x y. P x y}"
 by blast
 
-text{*actually a macro!*}
+text\<open>actually a macro!\<close>
 
 lemma "range f = f`UNIV"
 by blast
 
 
-text{*
+text\<open>
 inverse image
-*}
+\<close>
 
-text{*
+text\<open>
 @{thm[display] vimage_def[no_vars]}
 \rulename{vimage_def}
 
 @{thm[display] vimage_Compl[no_vars]}
 \rulename{vimage_Compl}
-*}
+\<close>
 
 
 end