13 trace_rewrite:=false; |
13 trace_rewrite:=false; |
14 *) |
14 *) |
15 val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x"; |
15 val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x"; |
16 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
16 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
17 if (term2str t) = "False" then () |
17 if (term2str t) = "False" then () |
18 else raise error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
18 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
19 |
19 |
20 val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; |
20 val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; |
21 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
21 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
22 if (term2str t) = "False" then () |
22 if (term2str t) = "False" then () |
23 else raise error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
23 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
24 |
24 |
25 val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; |
25 val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; |
26 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
26 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
27 if (term2str t) = "False" then () |
27 if (term2str t) = "False" then () |
28 else raise error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
28 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
29 |
29 |
30 val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; |
30 val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; |
31 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
31 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
32 if (term2str t) = "True" then () |
32 if (term2str t) = "True" then () |
33 else raise error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
33 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
34 |
34 |
35 val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
35 val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
36 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
36 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
37 if (term2str t) = "True" then () |
37 if (term2str t) = "True" then () |
38 else raise error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
38 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
39 |
39 |
40 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
40 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; |
41 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
41 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
42 if (term2str t) = "True" then () |
42 if (term2str t) = "True" then () |
43 else raise error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
43 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
44 |
44 |
45 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; |
45 val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; |
46 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
46 val SOME (t,_) = rewrite_set_ RootRatEq.thy false RootRatEq_prls t1; |
47 if (term2str t) = "True" then () |
47 if (term2str t) = "True" then () |
48 else raise error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
48 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
49 |
49 |
50 |
50 |
51 "--------------------- test thm rootrat_equation_left_1 ---------------------"; |
51 "--------------------- test thm rootrat_equation_left_1 ---------------------"; |
52 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"]; |
52 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"]; |
53 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
53 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
79 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
79 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
80 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
80 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
81 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
81 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
82 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
82 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
83 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then () |
83 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then () |
84 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_1"; |
84 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1"; |
85 (*-> Subproblem ("RootEq", ["polynomial", ...])*) |
85 (*-> Subproblem ("RootEq", ["polynomial", ...])*) |
86 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
86 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
87 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
87 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
88 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
88 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
89 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
89 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
92 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
92 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
93 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
93 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
94 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
94 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
95 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
95 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
96 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => () |
96 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => () |
97 | _ => raise error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]"; |
97 | _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]"; |
98 |
98 |
99 "--------------------- test thm rootrat_equation_left_2 ---------------------"; |
99 "--------------------- test thm rootrat_equation_left_2 ---------------------"; |
100 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"]; |
100 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"]; |
101 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
101 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
102 |
102 |
126 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
126 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
127 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
127 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
128 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
128 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
129 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
129 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
130 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then () |
130 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then () |
131 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_2"; |
131 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_2"; |
132 (*-> Subproblem ("PolyEq", ["polynomial", ...])*) |
132 (*-> Subproblem ("PolyEq", ["polynomial", ...])*) |
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
134 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
134 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
135 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
135 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
140 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
140 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
141 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
141 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
142 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
142 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
143 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => () |
143 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => () |
144 | _ => raise error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]"; |
144 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]"; |
145 |
145 |
146 "--------------------- test thm rootrat_equation_right_1 ---------------"; |
146 "--------------------- test thm rootrat_equation_right_1 ---------------"; |
147 val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"]; |
147 val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"]; |
148 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
148 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
149 |
149 |
169 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
169 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
170 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
170 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
171 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
171 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
172 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
172 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
173 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then () |
173 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + 4 * x = 0")) then () |
174 else raise error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1"; |
174 else error "rootrateq.sml: diff.behav.ppoly in rootrat_equation_right_1"; |
175 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
175 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
176 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
176 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
178 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
178 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
179 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
179 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
182 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
182 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
183 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
183 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
184 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
184 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
185 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
185 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
186 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => () |
186 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => () |
187 | _ => raise error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]"; |
187 | _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]"; |
188 |
188 |
189 "--------------------- test thm rootrat_equation_right_2 --------------------"; |
189 "--------------------- test thm rootrat_equation_right_2 --------------------"; |
190 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"]; |
190 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"]; |
191 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
191 val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]); |
192 |
192 |
211 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
211 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
212 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
212 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
213 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
213 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
214 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
214 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
215 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then () |
215 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-4 + x = 0")) then () |
216 else raise error "rootrateq.sml: diff.behav. in rootrat_equation_right_2"; |
216 else error "rootrateq.sml: diff.behav. in rootrat_equation_right_2"; |
217 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
217 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
218 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
218 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
219 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
219 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
220 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
220 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
221 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
221 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
224 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
224 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
225 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
225 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
226 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
226 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
227 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
227 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
228 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => () |
228 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => () |
229 | _ => raise error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]"; |
229 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]"; |