|
1 (* testexamples for RootratEq, equations mixing fractions and roots |
|
2 use"rootrateq.sml"; |
|
3 *) |
|
4 |
|
5 val thy = Isac.thy; |
|
6 |
|
7 "--------------------- tests on predicates -------------------------------"; |
|
8 "--------------------- tests on predicates -------------------------------"; |
|
9 "--------------------- tests on predicates -------------------------------"; |
|
10 (* |
|
11 Compiler.Control.Print.printDepth:=5; (*4 default*) |
|
12 trace_rewrite:=true; |
|
13 trace_rewrite:=false; |
|
14 *) |
|
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; |
|
17 if (term2str t) = "False" then () |
|
18 else raise error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; |
|
19 |
|
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; |
|
22 if (term2str t) = "False" then () |
|
23 else raise error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; |
|
24 |
|
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; |
|
27 if (term2str t) = "False" then () |
|
28 else raise error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; |
|
29 |
|
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; |
|
32 if (term2str t) = "True" then () |
|
33 else raise error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; |
|
34 |
|
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; |
|
37 if (term2str t) = "True" then () |
|
38 else raise error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; |
|
39 |
|
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; |
|
42 if (term2str t) = "True" then () |
|
43 else raise error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; |
|
44 |
|
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; |
|
47 if (term2str t) = "True" then () |
|
48 else raise error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; |
|
49 |
|
50 |
|
51 "--------------------- test thm rootrat_equation_left_1 ---------------------"; |
|
52 val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"]; |
|
53 val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]); |
|
54 |
|
55 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
56 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
57 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
58 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
59 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
60 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
61 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
62 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*) |
|
63 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
66 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
67 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
68 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
69 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*) |
|
70 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
71 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
72 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
73 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
74 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
75 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
76 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*) |
|
77 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
78 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; |
|
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; |
|
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"; |
|
85 (*-> Subproblem ("RootEq.thy", ["polynomial", ...])*) |
|
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; |
|
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; |
|
90 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
91 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; |
|
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; |
|
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]"; |
|
98 |
|
99 "--------------------- test thm rootrat_equation_left_2 ---------------------"; |
|
100 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"]; |
|
101 val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]); |
|
102 |
|
103 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
104 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
105 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
106 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
107 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
108 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
109 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*) |
|
110 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
111 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
112 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
113 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
114 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
115 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
116 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*) |
|
117 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
118 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
119 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
120 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
121 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
122 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
123 (*-> Subproblem ("RootEq.thy", ["univariate", ...])*) |
|
124 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
125 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; |
|
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; |
|
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"; |
|
132 (*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*) |
|
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; |
|
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; |
|
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
138 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; |
|
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; |
|
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]"; |
|
145 |
|
146 "--------------------- test thm rootrat_equation_right_1 ---------------"; |
|
147 val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"]; |
|
148 val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]); |
|
149 |
|
150 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
151 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
152 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
153 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
154 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
156 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
157 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
158 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
159 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
160 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
161 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
162 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
163 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
164 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
165 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
166 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
167 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
168 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; |
|
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; |
|
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"; |
|
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; |
|
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; |
|
179 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
180 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
181 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; |
|
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; |
|
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]"; |
|
188 |
|
189 "--------------------- test thm rootrat_equation_right_2 --------------------"; |
|
190 val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"]; |
|
191 val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]); |
|
192 |
|
193 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
194 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
195 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
196 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
197 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
198 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
199 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
200 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
201 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
202 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
203 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
204 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
205 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
206 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
207 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
208 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
209 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
210 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; |
|
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; |
|
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"; |
|
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; |
|
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; |
|
221 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
222 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
223 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; |
|
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; |
|
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]"; |