ProgTutorial/Parsing.thy
changeset 286 ff0b3d87a551
parent 285 abe5306cacbe
child 287 4b75f40b3e6c
--- 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}