equal
deleted
inserted
replaced
17 (1) triggered ["RootEq", "solve_sq_root_equation"] first time, because wrong '' in |
17 (1) triggered ["RootEq", "solve_sq_root_equation"] first time, because wrong '' in |
18 (Try (Repeat (Rewrite_Set ''make_rooteq ''))) was found |
18 (Try (Repeat (Rewrite_Set ''make_rooteq ''))) was found |
19 (2) correction ''make_rooteq'' led further to "check_elementwise: no set 1 + sqrt x = 3" |
19 (2) correction ''make_rooteq'' led further to "check_elementwise: no set 1 + sqrt x = 3" |
20 Since the changeset seems have nothing todo with these errors, this indicates that |
20 Since the changeset seems have nothing todo with these errors, this indicates that |
21 (a) either method ["RootEq", "solve_sq_root_equation"] & Co are somewhat indeterministic |
21 (a) either method ["RootEq", "solve_sq_root_equation"] & Co are somewhat indeterministic |
22 (b) of this is a case of indeterminism due to "handle _" or something similar elementary. |
22 (b) of this is a case of indeterminism due to something elementary. |
23 |
23 |
24 *) |
24 *) |
25 val thy = @{theory "RootRatEq"}; |
25 val thy = @{theory "RootRatEq"}; |
26 |
26 |
27 "------------ tests on predicates -------------------------------"; |
27 "------------ tests on predicates -------------------------------"; |