neuper@37906: (* use"kbtest/wn.sml";
neuper@37906:    use"wn.sml";
neuper@37906: 
neuper@37906:    various test dependent on IsacKnowledge/ outside Test.thy, Test.ML*)
neuper@37906: 
neuper@37906: 
Walther@60565:  val t = TermC.parse_test @{context} "solve (a*x + b = c, x)";
Walther@60650:  TermC.atom_trace_detail @{context} t;
neuper@37906: (*
neuper@37906: "\n*** -------------"
neuper@37906: "\n*** Const ( Equation.solve, bool * real => bool list)"
neuper@37906: ...    ~~~~~   ~~~~~~~~*)