diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 18 17:19:18 2000 +0200
@@ -67,7 +67,7 @@
 
 text{*\noindent
 Because @{term af} is monotone in its second argument (and also its first, but
-that is irrelevant) @{term"af A"} has a least fixpoint:
+that is irrelevant) @{term"af A"} has a least fixed point:
 *};
 
 lemma mono_af: "mono(af A)";
@@ -108,7 +108,7 @@
 
 txt{*\noindent
 In contrast to the analogous property for @{term EF}, and just
-for a change, we do not use fixpoint induction but a weaker theorem,
+for a change, we do not use fixed point induction but a weaker theorem,
 @{thm[source]lfp_lowerbound}:
 @{thm[display]lfp_lowerbound[of _ "S",no_vars]}
 The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
@@ -403,7 +403,7 @@
 set operations are easily implemented. Only @{term lfp} requires a little thought.
 Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},
 @{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until
-a fixpoint is reached. It is actually possible to generate executable functional programs
+a fixed point is reached. It is actually possible to generate executable functional programs
 from HOL definitions, but that is beyond the scope of the tutorial.
 *}
 (*<*)end(*>*)