--- a/ProgTutorial/Parsing.thy Wed Jul 22 14:02:47 2009 +0200
+++ b/ProgTutorial/Parsing.thy Wed Jul 22 15:14:29 2009 +0200
@@ -1095,7 +1095,7 @@
"foo method for conjE and conjI"
text {*
- It defines the method @{text foobar}, which takes no arguments (therefore the
+ It defines the method @{text foo}, which takes no arguments (therefore the
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}