changeset 567 | f7c97e64cc2a |
parent 566 | 6103b0eadbf2 |
child 569 | f875a25aa72d |
--- a/ProgTutorial/Package/Ind_Interface.thy Tue May 14 17:45:13 2019 +0200 +++ b/ProgTutorial/Package/Ind_Interface.thy Thu May 16 19:56:12 2019 +0200 @@ -107,7 +107,7 @@ If we feed into the parser the string that corresponds to our definition of @{term even} and @{term odd} - @{ML_response [display,gray] + @{ML_matchresult [display,gray] "let val input = filtered_input (\"even and odd \" ^