--- a/ProgTutorial/Tactical.thy	Wed Jul 22 15:31:22 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sun Jul 26 13:06:55 2009 +0200
@@ -63,7 +63,7 @@
   \begin{readmore}
   To learn more about the function @{ML [index] prove in Goal} see \isccite{sec:results}
   and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
-  "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
+  "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
   tactics and tactic combinators; see also Chapters 3 and 4 in the old
   Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. 
   \end{readmore}
@@ -1058,7 +1058,7 @@
   (FIXME: say something about @{ML [index] COND} and COND')
   
   \begin{readmore}
-  Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
+  Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
   \end{readmore}