# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1248606415 -7200
# Node ID 08ffafe2585d154619387bbd8b371c3bf6639261
# Parent  d6e9fb662d686d1149b20431f409c4a6c3236e1b
adapted to changes in Isabelle

diff -r d6e9fb662d68 -r 08ffafe2585d ProgTutorial/Tactical.thy
--- 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}
 
diff -r d6e9fb662d68 -r 08ffafe2585d progtutorial.pdf
Binary file progtutorial.pdf has changed