equal
deleted
inserted
replaced
27 (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac_Knowledge") works ? |
27 (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac_Knowledge") works ? |
28 Refine.refine ["equality ((2 log x) = 3)", "solveFor x", "solutions L"] |
28 Refine.refine ["equality ((2 log x) = 3)", "solveFor x", "solutions L"] |
29 ["equation", "test"]; *) |
29 ["equation", "test"]; *) |
30 *) |
30 *) |
31 |
31 |
32 val t = TermC.parse_test @{context} "(2 log x)"; |
32 val t = ParseC.parse_test @{context} "(2 log x)"; |
33 val t = TermC.parse_test @{context} "(2 log x) = 3"; |
33 val t = ParseC.parse_test @{context} "(2 log x) = 3"; |
34 val t = TermC.parse_test @{context} "matches ((?a log x) = ?b) ((2 log x) = 3)"; |
34 val t = ParseC.parse_test @{context} "matches ((?a log x) = ?b) ((2 log x) = 3)"; |
35 TermC.atom_trace_detail @{context} t; |
35 TermC.atom_trace_detail @{context} t; |
36 |
36 |
37 |
37 |
38 val fmz = ["equality ((2 log x) = 3)", "solveFor x", "solutions L"]; |
38 val fmz = ["equality ((2 log x) = 3)", "solveFor x", "solutions L"]; |
39 val (dI',pI',mI') = |
39 val (dI',pI',mI') = |