ProgTutorial/Parsing.thy
changeset 244 dc95a56b1953
parent 241 29d4701c5ee1
child 250 ab9e09076462
--- 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