112 member op = [Pbl,Met] p_; (*= false*) |
112 member op = [Pbl,Met] p_; (*= false*) |
113 "~~~~~ fun do_next, args:"; (*stopped due to strange exn |
113 "~~~~~ fun do_next, args:"; (*stopped due to strange exn |
114 "check_elementwise: no set 1 = 2 + - 2 * sqrt x"*) |
114 "check_elementwise: no set 1 = 2 + - 2 * sqrt x"*) |
115 |
115 |
116 (*---- 2nd try: we investigate the script ["RootEq", "solve_sq_root_equation"] found via pbl*) |
116 (*---- 2nd try: we investigate the script ["RootEq", "solve_sq_root_equation"] found via pbl*) |
117 val t = TermC.str2term "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)"; |
117 val t = TermC.parse_test @{context} "((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v)"; |
118 val t = TermC.str2term ("((lhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x) |" ^ |
118 val t = TermC.parse_test @{context} ("((lhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x) |" ^ |
119 " ((rhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x)"); |
119 " ((rhs (1 = 2 * (1 + - 1 * sqrt x))) is_sqrtTerm_in x)"); |
120 val SOME (t, _) = rewrite_set_ thy true rooteq_srls t; |
120 val SOME (t, _) = rewrite_set_ thy true rooteq_srls t; |
121 UnparseC.term t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take |
121 UnparseC.term t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take |
122 [univariate,equation] and to refine to ["sq", "rootX", "univariate", "equation"] in 2002*) |
122 [univariate,equation] and to refine to ["sq", "rootX", "univariate", "equation"] in 2002*) |
123 |
123 |