196 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^ |
196 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^ |
197 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]"; |
197 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]"; |
198 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*); |
198 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*); |
199 (*if*) Tactic.for_specify' m; (*false*) |
199 (*if*) Tactic.for_specify' m; (*false*) |
200 (*loc_solve_ (mI,m) ptp; |
200 (*loc_solve_ (mI,m) ptp; |
201 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
201 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |
202 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp); |
202 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp); |
203 (*solve m (pt, pos); |
203 (*solve m (pt, pos); |
204 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
204 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |
205 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos)); |
205 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos)); |
206 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
206 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
207 val thy' = get_obj g_domID pt (par_pblobj pt p); |
207 val thy' = get_obj g_domID pt (par_pblobj pt p); |
208 val (is, sc) = resume_prog thy' (p,p_) pt; |
208 val (is, sc) = resume_prog thy' (p,p_) pt; |
209 val d = e_rls; |
209 val d = e_rls; |
210 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; |
210 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; |
211 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
211 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*) |
212 "~~~~~ fun locate_input_tactic, args:"; val () = (); |
212 "~~~~~ fun locate_input_tactic, args:"; val () = (); |
213 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) |
213 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) |
214 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*); |
214 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*); |
215 (*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) |
215 (*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) |
216 ... Accept_Tac1 ... is correct*) |
216 ... Accept_Tac1 ... is correct*) |