diff -r fb6c29a90003 -r d8c376662bb4 ProgTutorial/Recipes/Sat.thy --- a/ProgTutorial/Recipes/Sat.thy Mon Apr 30 12:36:32 2012 +0100 +++ b/ProgTutorial/Recipes/Sat.thy Mon Apr 30 14:43:52 2012 +0100 @@ -27,7 +27,7 @@ The function will return a propositional formula and a table. Suppose *} -ML{*val (pform, table) = +ML %grayML{*val (pform, table) = Prop_Logic.prop_formula_of_term @{term "A \ \A \ B"} Termtab.empty*} text {* @@ -51,7 +51,7 @@ Attempting to translate @{term "\x::nat. P x"} *} -ML{*val (pform', table') = +ML %grayML{*val (pform', table') = Prop_Logic.prop_formula_of_term @{term "\x::nat. P x"} Termtab.empty*} text {* @@ -121,4 +121,4 @@ *} -end \ No newline at end of file +end