equal
deleted
inserted
replaced
158 @{ML_response \<open>error "hallo"\<close> |
158 @{ML_response \<open>error "hallo"\<close> |
159 \<open>hallo\<close>} |
159 \<open>hallo\<close>} |
160 |
160 |
161 So as a rule of thumb, to facilitate result checking use prefer this order: |
161 So as a rule of thumb, to facilitate result checking use prefer this order: |
162 \begin{enumerate} |
162 \begin{enumerate} |
163 \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> |
163 \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> |
164 \item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close> |
164 \item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close> |
165 \item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close> |
165 \item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close> |
166 \item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close> |
166 \item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close> |
167 \end{enumerate} |
167 \end{enumerate} |
168 |
168 |