--- a/doc-src/TutorialI/CTL/Base.thy Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy Fri Oct 20 08:46:41 2000 +0200
@@ -1,6 +1,6 @@
(*<*)theory Base = Main:(*>*)
-section{*Case study: Verified model checkers*}
+section{*Case study: Verified model checking*}
text{*
Model checking is a very popular technique for the verification of finite
@@ -50,18 +50,20 @@
which is false.
Abstracting from this concrete example, we assume there is some type of
-states
+states:
*}
typedecl state
text{*\noindent
-which we merely declare rather than define because it is an implicit
-parameter of our model. Of course it would have been more generic to make
-@{typ state} a type parameter of everything but fixing @{typ state} as above
-reduces clutter.
-Similarly we declare an arbitrary but fixed transition system, i.e.\
-relation between states:
+Command \isacommand{typedecl} merely declares a new type but without
+defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
+about the type other than its existence. That is exactly what we need
+because @{typ state} really is an implicit parameter of our model. Of
+course it would have been more generic to make @{typ state} a type
+parameter of everything but declaring @{typ state} globally as above
+reduces clutter. Similarly we declare an arbitrary but fixed
+transition system, i.e.\ relation between states:
*}
consts M :: "(state \<times> state)set";