128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
131 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]")) |
131 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]")) |
132 andalso nxt = ("End_Proof'",End_Proof') then () |
132 andalso nxt = ("End_Proof'",End_Proof') then () |
133 else raise error "new behaviour in testexample rationals2.sml 1+2*x=0"; |
133 else error "new behaviour in testexample rationals2.sml 1+2*x=0"; |
134 |
134 |
135 (*---------------------------------*) |
135 (*---------------------------------*) |
136 "-------------- is_rootequ_in - SubProblem -------------------------"; |
136 "-------------- is_rootequ_in - SubProblem -------------------------"; |
137 "-------------- is_rootequ_in - SubProblem -------------------------"; |
137 "-------------- is_rootequ_in - SubProblem -------------------------"; |
138 "-------------- is_rootequ_in - SubProblem -------------------------"; |
138 "-------------- is_rootequ_in - SubProblem -------------------------"; |
164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
166 if p = ([1,1],Frm) andalso |
166 if p = ([1,1],Frm) andalso |
167 f = Form' (FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso |
167 f = Form' (FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso |
168 nxt = ("Empty_Tac",Empty_Tac) (*script ist noch 'helpless'*) then () |
168 nxt = ("Empty_Tac",Empty_Tac) (*script ist noch 'helpless'*) then () |
169 else raise error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0"; |
169 else error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0"; |