diff -r abe5306cacbe -r ff0b3d87a551 ProgTutorial/Parsing.thy --- 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}