63 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
63 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; |
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; |
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; |
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; |
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; |
68 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
69 (*============ inhibit exn WN120319 ============================================== |
|
70 (*From final Test_Isac.thy we suddenly have |
|
71 |
|
72 nxt = ("Model_Problem", Model_Problem) |
|
73 |
|
74 which we did not investigate further due to the decision to drop the whole type of equation. |
|
75 *) |
69 if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then () |
76 if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then () |
70 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a"; |
77 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a"; |
71 (*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"])*) |
78 (*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"])*) |
72 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; |
73 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; |
154 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; |
155 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; |
156 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => () |
163 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => () |
157 | _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]"; |
164 | _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]"; |
158 ============ inhibit exn WN120314 ==============================================*) |
165 ============ inhibit exn WN120314 ==============================================*) |
|
166 ============ inhibit exn WN120319 ==============================================*) |
159 |
167 |
160 "------------ test thm rootrat_equation_left_2 -------------------"; |
168 "------------ test thm rootrat_equation_left_2 -------------------"; |
161 "------------ test thm rootrat_equation_left_2 -------------------"; |
169 "------------ test thm rootrat_equation_left_2 -------------------"; |
162 "------------ test thm rootrat_equation_left_2 -------------------"; |
170 "------------ test thm rootrat_equation_left_2 -------------------"; |
163 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"]; |
171 val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"]; |