equal
deleted
inserted
replaced
53 as a loose bound variable in the body, then we delete the quantifier. |
53 as a loose bound variable in the body, then we delete the quantifier. |
54 For this we have to increase all other dangling de Bruijn indices by |
54 For this we have to increase all other dangling de Bruijn indices by |
55 \<open>-1\<close> to account for the deleted quantifier. An example is |
55 \<open>-1\<close> to account for the deleted quantifier. An example is |
56 as follows: |
56 as follows: |
57 |
57 |
58 @{ML_response_fake [display,gray] |
58 @{ML_matchresult_fake [display,gray] |
59 "@{prop \"\<forall>x y z. P x = P z\"} |
59 "@{prop \"\<forall>x y z. P x = P z\"} |
60 |> kill_trivial_quantifiers |
60 |> kill_trivial_quantifiers |
61 |> pretty_term @{context} |
61 |> pretty_term @{context} |
62 |> pwriteln" |
62 |> pwriteln" |
63 "\<forall>x z. P x = P z"} |
63 "\<forall>x z. P x = P z"} |
108 text \<open> |
108 text \<open> |
109 By using \<open>#> fst\<close> in the last line, the function |
109 By using \<open>#> fst\<close> in the last line, the function |
110 @{ML scan_all} retruns a string, instead of the pair a parser would |
110 @{ML scan_all} retruns a string, instead of the pair a parser would |
111 normally return. For example: |
111 normally return. For example: |
112 |
112 |
113 @{ML_response [display,gray] |
113 @{ML_matchresult [display,gray] |
114 "let |
114 "let |
115 val input1 = (Symbol.explode \"foo bar\") |
115 val input1 = (Symbol.explode \"foo bar\") |
116 val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\") |
116 val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\") |
117 in |
117 in |
118 (scan_all input1, scan_all input2) |
118 (scan_all input1, scan_all input2) |
328 end\<close> |
328 end\<close> |
329 |
329 |
330 text \<open> |
330 text \<open> |
331 This function generates for example: |
331 This function generates for example: |
332 |
332 |
333 @{ML_response_fake [display,gray] |
333 @{ML_matchresult_fake [display,gray] |
334 "pwriteln (pretty_term @{context} (term_tree 2))" |
334 "pwriteln (pretty_term @{context} (term_tree 2))" |
335 "(1 + 2) + (3 + 4)"} |
335 "(1 + 2) + (3 + 4)"} |
336 |
336 |
337 The next function constructs a goal of the form \<open>P \<dots>\<close> with a term |
337 The next function constructs a goal of the form \<open>P \<dots>\<close> with a term |
338 produced by @{ML term_tree} filled in. |
338 produced by @{ML term_tree} filled in. |