4 *) |
4 *) |
5 |
5 |
6 theory T2_Rewriting imports Isac.Isac |
6 theory T2_Rewriting imports Isac.Isac |
7 begin |
7 begin |
8 |
8 |
9 chapter {* Rewriting *} |
9 chapter \<open>Rewriting\<close> |
10 |
10 |
11 text {* \emph{Rewriting} is a technique of Symbolic Computation, which is |
11 text \<open>\emph{Rewriting} is a technique of Symbolic Computation, which is |
12 appropriate to make a 'transparent system', because it is intuitively |
12 appropriate to make a 'transparent system', because it is intuitively |
13 comprehensible. For a thourogh introduction see the book of Tobias Nipkow, |
13 comprehensible. For a thourogh introduction see the book of Tobias Nipkow, |
14 http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/ |
14 http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/ |
15 |
15 |
16 section {* Introduction to rewriting *} |
16 section {* Introduction to rewriting\<close> |
17 |
17 |
18 text {* Rewriting creates calculations which look like written by hand; see the |
18 text \<open>Rewriting creates calculations which look like written by hand; see the |
19 ISAC tutoring system ! ISAC finds the rules automatically. Here we start by |
19 ISAC tutoring system ! ISAC finds the rules automatically. Here we start by |
20 telling the rules ourselves. |
20 telling the rules ourselves. |
21 Let's differentiate after we have identified the rules for differentiation, as |
21 Let's differentiate after we have identified the rules for differentiation, as |
22 found in ~~/src/Tools/isac/Knowledge/Diff.thy: |
22 found in ~~/src/Tools/isac/Knowledge/Diff.thy: |
23 *} |
23 \<close> |
24 ML {* |
24 ML \<open> |
25 val diff_sum = TermC.num_str @{thm diff_sum}; |
25 val diff_sum = TermC.num_str @{thm diff_sum}; |
26 val diff_pow = TermC.num_str @{thm diff_pow}; |
26 val diff_pow = TermC.num_str @{thm diff_pow}; |
27 val diff_var = TermC.num_str @{thm diff_var}; |
27 val diff_var = TermC.num_str @{thm diff_var}; |
28 val diff_const = TermC.num_str @{thm diff_const}; |
28 val diff_const = TermC.num_str @{thm diff_const}; |
29 *} |
29 \<close> |
30 text {* Looking at the rules (abbreviated by 'thm' above), we see the |
30 text \<open>Looking at the rules (abbreviated by 'thm' above), we see the |
31 differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound |
31 differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound |
32 variable. |
32 variable. |
33 Can you read diff_const in the Ouput window ? |
33 Can you read diff_const in the Ouput window ? |
34 |
34 |
35 Please, skip this introductory ML-section in the first go ...*} |
35 Please, skip this introductory ML-section in the first go ...\<close> |
36 ML {* |
36 ML \<open> |
37 (*default_print_depth 1;*) |
37 (*default_print_depth 1;*) |
38 val (thy, ro, er, inst) = |
38 val (thy, ro, er, inst) = |
39 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
39 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]); |
40 *} |
40 \<close> |
41 text {* ... and let us differentiate the term t: *} |
41 text \<open>... and let us differentiate the term t:\<close> |
42 ML {* |
42 ML \<open> |
43 val t = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x^^^2 + x + y)"; |
43 val t = (Thm.term_of o the o (TermC.parse thy)) "d_d x (x^^^2 + x + y)"; |
44 |
44 |
45 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; Rule.term2str t; |
45 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; Rule.term2str t; |
46 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; Rule.term2str t; |
46 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_sum t; Rule.term2str t; |
47 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_pow t; Rule.term2str t; |
47 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_pow t; Rule.term2str t; |
48 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_var t; Rule.term2str t; |
48 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_var t; Rule.term2str t; |
49 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_const t; Rule.term2str t; |
49 val SOME (t, _) = Rewrite.rewrite_inst_ thy ro er true inst diff_const t; Rule.term2str t; |
50 *} |
50 \<close> |
51 text {* Please, scoll up the Output-window to check the 5 steps of rewriting ! |
51 text \<open>Please, scoll up the Output-window to check the 5 steps of rewriting ! |
52 You might not be satisfied by the result "2 * x ^^^ (2 - 1) + 1 + 0". |
52 You might not be satisfied by the result "2 * x ^^^ (2 - 1) + 1 + 0". |
53 |
53 |
54 ISAC has a set of rules called 'make_polynomial', which simplifies the result: |
54 ISAC has a set of rules called 'make_polynomial', which simplifies the result: |
55 *} |
55 \<close> |
56 ML {* |
56 ML \<open> |
57 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; Rule.term2str t; |
57 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; Rule.term2str t; |
58 Celem.trace_rewrite := false; |
58 Celem.trace_rewrite := false; |
59 *} |
59 \<close> |
60 |
60 |
61 section {* Note on bound variables *} |
61 section \<open>Note on bound variables\<close> |
62 text {* You may have noticed that rewrite_ above could distinguish between x |
62 text \<open>You may have noticed that rewrite_ above could distinguish between x |
63 (d_d x x = 1) and y (d_d x y = 0). ISAC does this by instantiating theorems |
63 (d_d x x = 1) and y (d_d x y = 0). ISAC does this by instantiating theorems |
64 before application: given [(@{term "bdv::real"}, @{term "x::real"})] the |
64 before application: given [(@{term "bdv::real"}, @{term "x::real"})] the |
65 theorem diff_sum becomes "d_d x (?u + ?v) = d_d x ?u + d_d x ?v". |
65 theorem diff_sum becomes "d_d x (?u + ?v) = d_d x ?u + d_d x ?v". |
66 |
66 |
67 Isabelle does this differently by variables bound by a 'lambda' %, see |
67 Isabelle does this differently by variables bound by a 'lambda' %, see |
68 http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html |
68 http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html |
69 *} |
69 \<close> |
70 ML {* |
70 ML \<open> |
71 val t = @{term "%x. x^2 + x + y"}; TermC.atomwy t; Rule.term2str t; |
71 val t = @{term "%x. x^2 + x + y"}; TermC.atomwy t; Rule.term2str t; |
72 *} |
72 \<close> |
73 text {* Since this notation does not conform to present high-school matheatics |
73 text \<open>Since this notation does not conform to present high-school matheatics |
74 ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation |
74 ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation |
75 solving in ISAC. |
75 solving in ISAC. |
76 *} |
76 \<close> |
77 |
77 |
78 section {* Conditional and ordered rewriting *} |
78 section \<open>Conditional and ordered rewriting\<close> |
79 text {* We have already seen conditional rewriting above when we used the rule |
79 text \<open>We have already seen conditional rewriting above when we used the rule |
80 diff_const; let us try: *} |
80 diff_const; let us try:\<close> |
81 ML {* |
81 ML \<open> |
82 val t1 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*x*z)"; |
82 val t1 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*x*z)"; |
83 Rewrite.rewrite_inst_ thy ro er true inst diff_const t1; |
83 Rewrite.rewrite_inst_ thy ro er true inst diff_const t1; |
84 |
84 |
85 val t2 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*y*z)"; |
85 val t2 = (Thm.term_of o the o (TermC.parse thy)) "d_d x (a*BC*y*z)"; |
86 Rewrite.rewrite_inst_ thy ro er true inst diff_const t2; |
86 Rewrite.rewrite_inst_ thy ro er true inst diff_const t2; |
87 *} |
87 \<close> |
88 text {* For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false, |
88 text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false, |
89 since x occurs in t1 actually; thus the rule following implication '==>' is |
89 since x occurs in t1 actually; thus the rule following implication '==>' is |
90 not applied and rewrite_inst_ returns NONE. |
90 not applied and rewrite_inst_ returns NONE. |
91 For term t2 is 'not (x occurs_in "a*BC*y*z")' true, thus the rule is applied. |
91 For term t2 is 'not (x occurs_in "a*BC*y*z")' true, thus the rule is applied. |
92 *} |
92 \<close> |
93 |
93 |
94 subsection {* ordered rewriting *} |
94 subsection \<open>ordered rewriting\<close> |
95 text {* Let us start with an example; in order to see what is going on we tell |
95 text \<open>Let us start with an example; in order to see what is going on we tell |
96 Isabelle to show all brackets: |
96 Isabelle to show all brackets: |
97 *} |
97 \<close> |
98 ML {* |
98 ML \<open> |
99 (*show_brackets := true; TODO*) |
99 (*show_brackets := true; TODO*) |
100 val t0 = (Thm.term_of o the o (TermC.parse thy)) "2*a + 3*b + 4*a"; Rule.term2str t0; |
100 val t0 = (Thm.term_of o the o (TermC.parse thy)) "2*a + 3*b + 4*a"; Rule.term2str t0; |
101 (*show_brackets := false;*) |
101 (*show_brackets := false;*) |
102 *} |
102 \<close> |
103 text {* Now we want to bring 4*a close to 2*a in order to get 6*a: |
103 text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a: |
104 *} |
104 \<close> |
105 ML {* |
105 ML \<open> |
106 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.assoc} t0; Rule.term2str t; |
106 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.assoc} t0; Rule.term2str t; |
107 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.left_commute} t; Rule.term2str t; |
107 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.left_commute} t; Rule.term2str t; |
108 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t; |
108 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t; |
109 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm real_num_collect} t; Rule.term2str t; |
109 val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm real_num_collect} t; Rule.term2str t; |
110 *} |
110 \<close> |
111 text {* That is fine, we just need to add 2+4 !!!!! See the next section below. |
111 text \<open>That is fine, we just need to add 2+4 !!!!! See the next section below. |
112 |
112 |
113 But we cannot automate such ordering with what we know so far: If we put |
113 But we cannot automate such ordering with what we know so far: If we put |
114 add.assoc, add.left_commute and add.commute into one ruleset (your have used |
114 add.assoc, add.left_commute and add.commute into one ruleset (your have used |
115 ruleset 'make_polynomial' already), then all the rules are applied as long |
115 ruleset 'make_polynomial' already), then all the rules are applied as long |
116 as one rule is applicable (that is the way such rulesets work). |
116 as one rule is applicable (that is the way such rulesets work). |
117 Try to step through the ML-sections without skipping one of them ... |
117 Try to step through the ML-sections without skipping one of them ... |
118 *} |
118 \<close> |
119 ML {*val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t*} |
119 ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t\<close> |
120 ML {*val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t*} |
120 ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t\<close> |
121 ML {*val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t*} |
121 ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t\<close> |
122 ML {*val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t*} |
122 ML \<open>val SOME (t, _) = Rewrite.rewrite_ thy ro er true @{thm add.commute} t; Rule.term2str t\<close> |
123 text {* ... you can go forever, the ruleset is 'not terminating'. |
123 text \<open>... you can go forever, the ruleset is 'not terminating'. |
124 The theory of rewriting makes this kind of rulesets terminate by the use of |
124 The theory of rewriting makes this kind of rulesets terminate by the use of |
125 'rewrite orders': |
125 'rewrite orders': |
126 Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then |
126 Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then |
127 'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only |
127 'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only |
128 applied, when the result t2 is 'smaller', '<', than the one to be rewritten. |
128 applied, when the result t2 is 'smaller', '<', than the one to be rewritten. |
129 Defining such a '<' is not trivial, see ~~/src/Tools/isacKnowledge/Poly.thy |
129 Defining such a '<' is not trivial, see ~~/src/Tools/isacKnowledge/Poly.thy |
130 for 'fun has_degree_in' etc. |
130 for 'fun has_degree_in' etc. |
131 *} |
131 \<close> |
132 |
132 |
133 subsection {* Simplification in ISAC *} |
133 subsection \<open>Simplification in ISAC\<close> |
134 text {* |
134 text \<open> |
135 With the introduction into rewriting, ordered rewriting and conditional |
135 With the introduction into rewriting, ordered rewriting and conditional |
136 rewriting we have seen all what is necessary for the practice of rewriting. |
136 rewriting we have seen all what is necessary for the practice of rewriting. |
137 |
137 |
138 One basic technique of 'symbolic computation' which uses rewriting is |
138 One basic technique of 'symbolic computation' which uses rewriting is |
139 simplification, that means: transform terms into an equivalent form which is |
139 simplification, that means: transform terms into an equivalent form which is |
141 Isabelle has powerful and efficient simplifiers. Nevertheless, ISAC has another |
141 Isabelle has powerful and efficient simplifiers. Nevertheless, ISAC has another |
142 kind of simplifiers, which groups rulesets such that the trace of rewrites is |
142 kind of simplifiers, which groups rulesets such that the trace of rewrites is |
143 more readable in ISAC's worksheets. |
143 more readable in ISAC's worksheets. |
144 |
144 |
145 Here are examples of of how ISAC's simplifier work: |
145 Here are examples of of how ISAC's simplifier work: |
146 *} |
146 \<close> |
147 ML {* |
147 ML \<open> |
148 (*show_brackets := false; TODO*) |
148 (*show_brackets := false; TODO*) |
149 val t1 = (Thm.term_of o the o (TermC.parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)"; |
149 val t1 = (Thm.term_of o the o (TermC.parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)"; |
150 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t1; Rule.term2str t; |
150 val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t1; Rule.term2str t; |
151 *} |
151 \<close> |
152 ML {* |
152 ML \<open> |
153 val t2 = (Thm.term_of o the o (TermC.parse thy)) |
153 val t2 = (Thm.term_of o the o (TermC.parse thy)) |
154 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))"; |
154 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))"; |
155 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; Rule.term2str t; |
155 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; Rule.term2str t; |
156 *} |
156 \<close> |
157 text {* The simplifiers are quite busy when finding the above results. you can |
157 text \<open>The simplifiers are quite busy when finding the above results. you can |
158 watch them at work by setting the switch 'trace_rewrite:*} |
158 watch them at work by setting the switch 'trace_rewrite:\<close> |
159 ML {* |
159 ML \<open> |
160 Celem.trace_rewrite := false; |
160 Celem.trace_rewrite := false; |
161 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
161 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
162 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; Rule.term2str t; |
162 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; Rule.term2str t; |
163 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
163 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++"; |
164 Celem.trace_rewrite := false; |
164 Celem.trace_rewrite := false; |
165 *} |
165 \<close> |
166 text {* You see what happend when you click the checkbox <Tracing> on the bar |
166 text \<open>You see what happend when you click the checkbox <Tracing> on the bar |
167 separating this window from the Output-window. |
167 separating this window from the Output-window. |
168 |
168 |
169 So, it might be better to take simpler examples for watching the simplifiers. |
169 So, it might be better to take simpler examples for watching the simplifiers. |
170 *} |
170 \<close> |
171 |
171 |
172 |
172 |
173 section {* Experiments with a simplifier conserving minus *} |
173 section \<open>Experiments with a simplifier conserving minus\<close> |
174 |
174 |
175 text {* We conclude the section on rewriting with starting into an experimental |
175 text \<open>We conclude the section on rewriting with starting into an experimental |
176 development. This development has been urged by teachers using ISAC for |
176 development. This development has been urged by teachers using ISAC for |
177 introduction to algebra with students at the age of 12-14. |
177 introduction to algebra with students at the age of 12-14. |
178 |
178 |
179 The teachers requested ISAC to keep the minus, for instance in the above |
179 The teachers requested ISAC to keep the minus, for instance in the above |
180 result "a^3 + -1 * b^3" (here ISAC should write "a^3 - * b^3") and also |
180 result "a^3 + -1 * b^3" (here ISAC should write "a^3 - * b^3") and also |
181 in all intermediate steps. |
181 in all intermediate steps. |
182 |
182 |
183 So we started to develop (in German !) such a simplifier in |
183 So we started to develop (in German !) such a simplifier in |
184 ~~/src/Tools/isac/Knowledge/PolyMinus.thy |
184 ~~/src/Tools/isac/Knowledge/PolyMinus.thy |
185 *} |
185 \<close> |
186 |
186 |
187 subsection {* What already works *} |
187 subsection \<open>What already works\<close> |
188 ML {* |
188 ML \<open> |
189 val t2 = (Thm.term_of o the o (TermC.parse thy)) |
189 val t2 = (Thm.term_of o the o (TermC.parse thy)) |
190 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; |
190 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; |
191 val SOME (t, _) = Rewrite.rewrite_set_ thy true rls_p_33 t2; Rule.term2str t; |
191 val SOME (t, _) = Rewrite.rewrite_set_ thy true rls_p_33 t2; Rule.term2str t; |
192 *} |
192 \<close> |
193 text {* Try your own examples ! *} |
193 text \<open>Try your own examples !\<close> |
194 |
194 |
195 subsection {* This raises questions about didactics *} |
195 subsection \<open>This raises questions about didactics\<close> |
196 text {* Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy |
196 text \<open>Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy |
197 *} |
197 \<close> |
198 ML {* |
198 ML \<open> |
199 @{thm subtrahiere}; |
199 @{thm subtrahiere}; |
200 @{thm subtrahiere_von_1}; |
200 @{thm subtrahiere_von_1}; |
201 @{thm subtrahiere_1}; |
201 @{thm subtrahiere_1}; |
202 *} |
202 \<close> |
203 text {* That would not be so bad. But it is only a little part of what else is |
203 text \<open>That would not be so bad. But it is only a little part of what else is |
204 required: |
204 required: |
205 *} |
205 \<close> |
206 ML {* |
206 ML \<open> |
207 @{thm subtrahiere_x_plus_minus}; |
207 @{thm subtrahiere_x_plus_minus}; |
208 @{thm subtrahiere_x_plus1_minus}; |
208 @{thm subtrahiere_x_plus1_minus}; |
209 @{thm subtrahiere_x_plus_minus1}; |
209 @{thm subtrahiere_x_plus_minus1}; |
210 @{thm subtrahiere_x_minus_plus}; |
210 @{thm subtrahiere_x_minus_plus}; |
211 @{thm subtrahiere_x_minus1_plus}; |
211 @{thm subtrahiere_x_minus1_plus}; |
212 @{thm subtrahiere_x_minus_plus1}; |
212 @{thm subtrahiere_x_minus_plus1}; |
213 @{thm subtrahiere_x_minus_minus}; |
213 @{thm subtrahiere_x_minus_minus}; |
214 @{thm subtrahiere_x_minus1_minus}; |
214 @{thm subtrahiere_x_minus1_minus}; |
215 @{thm subtrahiere_x_minus_minus1}; |
215 @{thm subtrahiere_x_minus_minus1}; |
216 *} |
216 \<close> |
217 text {* So, learning so many rules, and learning to apply these rules, is futile. |
217 text \<open>So, learning so many rules, and learning to apply these rules, is futile. |
218 Actually, most of our students are unable to apply theorems. |
218 Actually, most of our students are unable to apply theorems. |
219 |
219 |
220 But if you look at 'make_polynomial' or even 'norm_Rational' you see, |
220 But if you look at 'make_polynomial' or even 'norm_Rational' you see, |
221 that these general simplifiers require about 10% than rulesets for '-'. |
221 that these general simplifiers require about 10% than rulesets for '-'. |
222 |
222 |
223 So, we might have better chances to teach our student to apply theorems |
223 So, we might have better chances to teach our student to apply theorems |
224 without '-' ? |
224 without '-' ? |
225 *} |
225 \<close> |
226 |
226 |
227 subsection {* This does not yet work *} |
227 subsection \<open>This does not yet work\<close> |
228 ML {* |
228 ML \<open> |
229 val t = (Thm.term_of o the o (TermC.parse thy)) |
229 val t = (Thm.term_of o the o (TermC.parse thy)) |
230 "(2*a - 5*b) * (2*a + 5*b)"; |
230 "(2*a - 5*b) * (2*a + 5*b)"; |
231 Rewrite.rewrite_set_ thy true rls_p_33 t; Rule.term2str t; |
231 Rewrite.rewrite_set_ thy true rls_p_33 t; Rule.term2str t; |
232 *} |
232 \<close> |
233 |
233 |
234 end |
234 end |