equal
deleted
inserted
replaced
203 fix two variables: |
203 fix two variables: |
204 *} |
204 *} |
205 |
205 |
206 lemma "True" |
206 lemma "True" |
207 proof - |
207 proof - |
208 txt_raw {*\mbox{}\\[-7mm]*} |
|
209 ML_prf {* Variable.dest_fixes @{context} *} |
208 ML_prf {* Variable.dest_fixes @{context} *} |
210 txt_raw {*\mbox{}\\[-7mm]\mbox{}*} |
209 fix x y |
211 fix x y |
210 ML_prf {* Variable.dest_fixes @{context} *}(*<*)oops(*>*) |
212 txt_raw {*\mbox{}\\[-7mm]*} |
|
213 ML_prf {* Variable.dest_fixes @{context} *} |
|
214 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
|
215 |
211 |
216 text {* |
212 text {* |
217 The interesting point is that we injected ML-code before and after |
213 The interesting point is that we injected ML-code before and after |
218 the variables are fixed. For this remember that ML-code inside a proof |
214 the variables are fixed. For this remember that ML-code inside a proof |
219 needs to be enclosed inside \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"}, |
215 needs to be enclosed inside \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"}, |
230 |
226 |
231 lemma "True" |
227 lemma "True" |
232 proof - |
228 proof - |
233 fix x y |
229 fix x y |
234 { fix z w |
230 { fix z w |
235 txt_raw {*\mbox{}\\[-7mm]*} |
231 ML_prf {* Variable.dest_fixes @{context} *} |
236 ML_prf {* Variable.dest_fixes @{context} *} |
232 } |
237 txt_raw {*\mbox{}\\[-7mm]\mbox{}*} |
233 ML_prf {* Variable.dest_fixes @{context} *}(*<*)oops(*>*) |
238 } |
|
239 txt_raw {*\mbox{}\\[-7mm]*} |
|
240 ML_prf {* Variable.dest_fixes @{context} *} |
|
241 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
|
242 |
234 |
243 text {* |
235 text {* |
244 Here the first time we call @{ML dest_fixes in Variable} we have four fixes variables; |
236 Here the first time we call @{ML dest_fixes in Variable} we have four fixes variables; |
245 the second time we get only the fixes variables @{text x} and @{text y} as answer, since |
237 the second time we get only the fixes variables @{text x} and @{text y} as answer, since |
246 @{text z} and @{text w} are not anymore in the scope of the context. |
238 @{text z} and @{text w} are not anymore in the scope of the context. |