equal
deleted
inserted
replaced
105 deal with them. Later, however, we will come back to them. |
105 deal with them. Later, however, we will come back to them. |
106 |
106 |
107 If we feed into the parser the string that corresponds to our definition |
107 If we feed into the parser the string that corresponds to our definition |
108 of @{term even} and @{term odd} |
108 of @{term even} and @{term odd} |
109 |
109 |
110 @{ML_response [display,gray] |
110 @{ML_matchresult [display,gray] |
111 "let |
111 "let |
112 val input = filtered_input |
112 val input = filtered_input |
113 (\"even and odd \" ^ |
113 (\"even and odd \" ^ |
114 \"where \" ^ |
114 \"where \" ^ |
115 \" even0[intro]: \\\"even 0\\\" \" ^ |
115 \" even0[intro]: \\\"even 0\\\" \" ^ |