diff -r 68105cf615fa -r 270b285d48ee doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Mon Nov 27 11:06:28 2000 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Mon Nov 27 16:40:56 2000 +0100
@@ -96,7 +96,7 @@
 
 apply(rule equalityI);
  apply(rule subsetI);
- apply(simp)
+ apply(simp)(*<*)apply(rename_tac s)(*>*)
 
 txt{*\noindent
 Simplification leaves us with the following first subgoal