--- a/doc-src/TutorialI/Overview/Sets.thy Fri Jun 21 15:41:07 2002 +0200
+++ b/doc-src/TutorialI/Overview/Sets.thy Fri Jun 21 18:40:06 2002 +0200
@@ -1,32 +1,42 @@
+(*<*)
theory Sets = Main:
-
+(*>*)
section{*Sets, Functions and Relations*}
subsection{*Set Notation*}
-term "A \<union> B"
-term "A \<inter> B"
-term "A - B"
-term "a \<in> A"
-term "b \<notin> A"
-term "{a,b}"
-term "{x. P x}"
-term "{x+y+eps |x y. x < y}"
-term "\<Union> M"
-term "\<Union>a \<in> A. F a"
+text{*
+\begin{center}
+\begin{tabular}{ccc}
+@{term "A \<union> B"} & @{term "A \<inter> B"} & @{term "A - B"} \\
+@{term "a \<in> A"} & @{term "b \<notin> A"} \\
+@{term "{a,b}"} & @{text "{x. P x}"} \\
+@{term "\<Union> M"} & @{text "\<Union>a \<in> A. F a"}
+\end{tabular}
+\end{center}
+*}
+
+subsection{*Some Functions*}
-subsection{*Functions*}
-
+text{*
+\begin{tabular}{l}
+@{thm id_def}\\
+@{thm o_def[no_vars]}\\
+@{thm image_def[no_vars]}\\
+@{thm vimage_def[no_vars]}
+\end{tabular}
+*}
+(*<*)
thm id_def
-thm o_assoc
-thm image_Int
-thm vimage_Compl
+thm o_def[no_vars]
+thm image_def[no_vars]
+thm vimage_def[no_vars]
+(*>*)
-
-subsection{*Relations*}
+subsection{*Some Relations*}
thm Id_def
-thm converse_comp
+thm converse_def
thm Image_def
thm relpow.simps
thm rtrancl_idemp
@@ -117,7 +127,6 @@
@{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
\end{exercise}
*}
-
+(*<*)
end
-
-
+(*>*)