--- a/doc-src/TutorialI/Overview/LNCS/Sets.thy Thu Aug 08 23:53:22 2002 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/Sets.thy Fri Aug 09 11:22:18 2002 +0200
@@ -18,6 +18,7 @@
term "{a,b}" term "{x. P x}"
term "\<Union> M" term "\<Union>a \<in> A. F a"(*>*)
+
subsection{*Some Functions*}
text{*
@@ -29,6 +30,7 @@
\end{tabular}*}
(*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*)
+
subsection{*Some Relations*}
text{*
@@ -47,6 +49,7 @@
thm rtrancl.intros[no_vars]
thm trancl_def[no_vars](*>*)
+
subsection{*Wellfoundedness*}
text{*
@@ -57,6 +60,7 @@
(*<*)thm wf_def[no_vars]
thm wf_iff_no_infinite_down_chain[no_vars](*>*)
+
subsection{*Fixed Point Operators*}
text{*
@@ -69,9 +73,9 @@
thm lfp_unfold
thm lfp_induct(*>*)
+
subsection{*Case Study: Verified Model Checking*}
-
typedecl state
consts M :: "(state \<times> state)set"
@@ -81,10 +85,10 @@
consts L :: "state \<Rightarrow> atom set"
datatype formula = Atom atom
- | Neg formula
- | And formula formula
- | AX formula
- | EF formula
+ | Neg formula
+ | And formula formula
+ | AX formula
+ | EF formula
consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)