diff -r efb5fff99c96 -r 6bce4acf7f2a ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Fri Aug 21 11:42:14 2009 +0200 +++ b/ProgTutorial/Parsing.thy Fri Aug 21 16:04:59 2009 +0200 @@ -1066,6 +1066,9 @@ *} + + + section {* Methods (TBD) *} text {* @@ -1110,6 +1113,10 @@ (*<*)oops(*>*) + + + + (* ML {* SIMPLE_METHOD *} ML {* METHOD *}