--- a/ProgTutorial/Solutions.thy	Tue Nov 17 18:40:11 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Tue Nov 17 20:36:18 2009 +0100
@@ -82,9 +82,25 @@
 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
 *}
 
-text {* \solution{ex:dyckhoff} *}
+text {* \solution{ex:contextfree} *}
+
+ML{*datatype expr = 
+   Number of int
+ | Mult of expr * expr 
+ | Add of expr * expr
 
-text {*
+fun parse_basic xs =
+  (OuterParse.nat >> Number 
+   || OuterParse.$$$ "(" |-- parse_expr --| OuterParse.$$$ ")") xs
+and parse_factor xs =
+  (parse_basic --| OuterParse.$$$ "*" -- parse_factor >> Mult 
+   || parse_basic) xs
+and parse_expr xs =
+  (parse_factor --| OuterParse.$$$ "+" -- parse_expr >> Add 
+   || parse_factor) xs*}
+
+
+text {* \solution{ex:dyckhoff} 
   The axiom rule can be implemented with the function @{ML atac}. The other
   rules correspond to the theorems: