--- a/ProgTutorial/Parsing.thy Wed Jul 22 15:14:29 2009 +0200
+++ b/ProgTutorial/Parsing.thy Wed Jul 22 15:15:22 2009 +0200
@@ -1099,7 +1099,7 @@
parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which
applies @{thm [source] conjE} and then @{thm [source] conjI}. The function
@{ML [index] SIMPLE_METHOD}
- turns such a tactic into a method. The method @{text "foobar"} can be used as follows
+ turns such a tactic into a method. The method @{text "foo"} can be used as follows
*}
lemma shows "A \<and> B \<Longrightarrow> C \<and> D"