diff -r 6e0f56764ff8 -r dc95a56b1953 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Wed Apr 29 00:36:14 2009 +0200 +++ b/ProgTutorial/Parsing.thy Tue May 05 03:21:49 2009 +0200 @@ -1078,10 +1078,10 @@ An example of a very simple method is: *} -method_setup %gray foobar = +method_setup %gray foo = {* Scan.succeed (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} - "foobar method for conjE and conjI" + "foo method for conjE and conjI" text {* It defines the method @{text foobar}, which takes no arguments (therefore the @@ -1091,7 +1091,7 @@ *} lemma shows "A \ B \ C \ D" -apply(foobar) +apply(foo) txt {* where it results in the goal state