equal
deleted
inserted
replaced
33 |
33 |
34 Please, skip this introductory ML-section in the first go ...*} |
34 Please, skip this introductory ML-section in the first go ...*} |
35 ML {* |
35 ML {* |
36 print_depth 1; |
36 print_depth 1; |
37 val (thy, ro, er, inst) = |
37 val (thy, ro, er, inst) = |
38 (theory "Isac", tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
38 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
39 *} |
39 *} |
40 text {* ... and let us differentiate the term t: *} |
40 text {* ... and let us differentiate the term t: *} |
41 ML {* |
41 ML {* |
42 val t = (term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)"; |
42 val t = (term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)"; |
43 |
43 |
93 subsection {* ordered rewriting *} |
93 subsection {* ordered rewriting *} |
94 text {* Let us start with an example; in order to see what is going on we tell |
94 text {* Let us start with an example; in order to see what is going on we tell |
95 Isabelle to show all brackets: |
95 Isabelle to show all brackets: |
96 *} |
96 *} |
97 ML {* |
97 ML {* |
98 show_brackets := true; |
98 (*show_brackets := true; TODO*) |
99 val t0 = (term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0; |
99 val t0 = (term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0; |
100 (*show_brackets := false;*) |
100 (*show_brackets := false;*) |
101 *} |
101 *} |
102 text {* Now we want to bring 4*a close to 2*a in order to get 6*a: |
102 text {* Now we want to bring 4*a close to 2*a in order to get 6*a: |
103 *} |
103 *} |
142 more readable in ISAC's worksheets. |
142 more readable in ISAC's worksheets. |
143 |
143 |
144 Here are examples of of how ISAC's simplifier work: |
144 Here are examples of of how ISAC's simplifier work: |
145 *} |
145 *} |
146 ML {* |
146 ML {* |
147 show_brackets := false; |
147 (*show_brackets := false; TODO*) |
148 val t1 = (term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)"; |
148 val t1 = (term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)"; |
149 val SOME (t, _) = rewrite_set_ thy true make_polynomial t1; term2str t; |
149 val SOME (t, _) = rewrite_set_ thy true make_polynomial t1; term2str t; |
150 *} |
150 *} |
151 ML {* |
151 ML {* |
152 val t2 = (term_of o the o (parse thy)) |
152 val t2 = (term_of o the o (parse thy)) |