src/Tools/isac/Knowledge/Root.thy
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;