changeset 60567 | bb3140a02f3d |
parent 60547 | 99328169539a |
child 60586 | 007ef64dbb08 |
1.1 --- a/src/Tools/isac/Knowledge/Root.thy Sun Oct 09 09:01:29 2022 +0200 1.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Oct 19 10:43:04 2022 +0200 1.3 @@ -69,7 +69,7 @@ 1.4 | NONE => NONE) 1.5 | _ => NONE); 1.6 1.7 -(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", str2term "sqrt 0"); 1.8 +(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", TermC.parse_test @{context} "sqrt 0"); 1.9 > eval_sqrt thmid op_ t thy; 1.10 > val Free (n1,t1) = arg; 1.11 > val SOME ni = int_of_str n1;