--- a/doc-src/TutorialI/CTL/CTL.thy Wed May 25 09:03:53 2005 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Wed May 25 09:04:24 2005 +0200
@@ -244,7 +244,7 @@
automatically. This is what happens in the step case.
The induction step is similar, but more involved, because now we face nested
-occurrences of @{const SOME}. As a result, @{text fast} is no longer able to
+occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely
show the proof commands but do not describe the details:
*};