| author | wneuper <Walther.Neuper@jku.at> |
| Wed, 11 Jan 2023 11:38:01 +0100 | |
| changeset 60650 | 06ec8abfd3bc |
| parent 60565 | f92963a33fe3 |
| child 60660 | c4b24621077e |
| permissions | -rw-r--r-- |
| neuper@37906 | 1 |
(* use"kbtest/wn.sml"; |
| neuper@37906 | 2 |
use"wn.sml"; |
| neuper@37906 | 3 |
|
| neuper@37906 | 4 |
various test dependent on IsacKnowledge/ outside Test.thy, Test.ML*) |
| neuper@37906 | 5 |
|
| neuper@37906 | 6 |
|
| Walther@60565 | 7 |
val t = TermC.parse_test @{context} "solve (a*x + b = c, x)";
|
| Walther@60650 | 8 |
TermC.atom_trace_detail @{context} t;
|
| neuper@37906 | 9 |
(* |
| neuper@37906 | 10 |
"\n*** -------------" |
| neuper@37906 | 11 |
"\n*** Const ( Equation.solve, bool * real => bool list)" |
| neuper@37906 | 12 |
... ~~~~~ ~~~~~~~~*) |