134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
135 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => () |
135 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => () |
136 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]"; |
136 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]"; |
137 if UnparseC.terms (*WN1104changed*) (Ctree.get_assumptions pt p) = "[0 <= 1 / 25]" |
137 if UnparseC.terms (*WN1104changed*) (Ctree.get_assumptions pt p) = "[0 <= 1 / 25]" |
138 (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..: |
138 (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..: |
139 [(TermC.str2term"25 ~= 0",[])] *) |
139 [(TermC.parse_test @{context}"25 ~= 0",[])] *) |
140 then writeln "should be True\n\ |
140 then writeln "should be True\n\ |
141 \should be True\n\ |
141 \should be True\n\ |
142 \should be True\n" |
142 \should be True\n" |
143 else error "rooteq.sml: diff.behav. with 25 ~= 0"; |
143 else error "rooteq.sml: diff.behav. with 25 ~= 0"; |
144 |
144 |
202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
203 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
203 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
205 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => () |
205 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => () |
206 | _ => error "rooteq.sml: diff.behav. [x = 4]"; |
206 | _ => error "rooteq.sml: diff.behav. [x = 4]"; |
207 if Ctree.get_assumptions pt p = [TermC.str2term"0 <= 12 * sqrt 2 * 4"] |
207 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"0 <= 12 * sqrt 2 * 4"] |
208 then writeln "should be True\nshould be True\nshould be True\n\ |
208 then writeln "should be True\nshould be True\nshould be True\n\ |
209 \should be True\nshould be True\nshould be True\n" |
209 \should be True\nshould be True\nshould be True\n" |
210 else error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4"; |
210 else error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4"; |
211 |
211 |
212 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------"; |
212 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------"; |