--- 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 \<and> B \<Longrightarrow> C \<and> D"
-apply(foobar)
+apply(foo)
txt {*
where it results in the goal state