1.1 --- a/src/Tools/isac/Knowledge/Root.thy	Tue Aug 17 21:48:38 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Tue Aug 17 21:57:40 2021 +0200
     1.3 @@ -44,37 +44,38 @@
     1.4  ML \<open>
     1.5  (*-------------------------functions---------------------*)
     1.6  (*evaluation square-root over the integers*)
     1.7 -fun eval_sqrt (_ : string) (_ : string) (t as (Const (op0, _) $ arg)) _(*thy*) = 
     1.8 -    (case arg of 
     1.9 -  	  (Const (\<^const_name>\<open>numeral\<close>, T) $ num) =>
    1.10 -        let val ni = HOLogic.dest_numeral num
    1.11 -        in
    1.12 -    	    if ni < 0 then NONE
    1.13 -    	    else
    1.14 -    		    let val fact = Eval.squfact ni;
    1.15 -    		    in
    1.16 +fun eval_sqrt (_ : string) (_ : string) t (_: theory) = 
    1.17 +  (case t of
    1.18 +    Const (op0, _) $ num =>
    1.19 +      (case try HOLogic.dest_number num of
    1.20 +        SOME (T, ni)=>
    1.21 +          if ni < 0 then NONE
    1.22 +          else
    1.23 +            let val fact = Eval.squfact ni;
    1.24 +            in
    1.25                if fact * fact = ni 
    1.26 -    		      then
    1.27 +              then
    1.28                  SOME ("#sqrt #" ^ string_of_int ni ^ " = #"
    1.29 -    			          ^ string_of_int (if ni = 0 then 0 else ni div fact),
    1.30 -    			        HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num T fact))
    1.31 -    		      else if fact = 1 then NONE
    1.32 -      		    else
    1.33 +                    ^ string_of_int (if ni = 0 then 0 else ni div fact),
    1.34 +                  HOLogic.Trueprop $ TermC.mk_equality (t, TermC.term_of_num T fact))
    1.35 +              else if fact = 1 then NONE
    1.36 +              else
    1.37                  SOME ("#sqrt #" ^ string_of_int ni ^ " = sqrt (#"
    1.38 -      		          ^ string_of_int fact ^ " * #" ^ string_of_int fact ^ " * #"
    1.39 -      		          ^ string_of_int (ni div (fact * fact)) ^ ")",
    1.40 -      		        HOLogic.Trueprop $ TermC.mk_equality 
    1.41 +                    ^ string_of_int fact ^ " * #" ^ string_of_int fact ^ " * #"
    1.42 +                    ^ string_of_int (ni div (fact * fact)) ^ ")",
    1.43 +                  HOLogic.Trueprop $ TermC.mk_equality 
    1.44                      (t, (TermC.mk_factroot op0 T fact (ni div (fact*fact)))))
    1.45 -    	      end
    1.46 -  	    end
    1.47 -    | _ => NONE)
    1.48 -  | eval_sqrt _ _ _ _ = NONE;
    1.49 +            end
    1.50 +        | NONE => NONE)
    1.51 +  | _ => NONE);
    1.52 +
    1.53  (*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", str2term "sqrt 0");
    1.54  > eval_sqrt thmid op_ t thy;
    1.55  > val Free (n1,t1) = arg; 
    1.56  > val SOME ni = int_of_str n1;
    1.57  *)
    1.58  \<close>
    1.59 +
    1.60  calculation SQRT (sqrt) = \<open>eval_sqrt "#sqrt_"\<close>
    1.61      (*different types for 'sqrt 4' --- 'Calculate SQRT'*)
    1.62  ML \<open>

     2.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Tue Aug 17 21:48:38 2021 +0200
     2.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Tue Aug 17 21:57:40 2021 +0200
     2.3 @@ -459,12 +459,8 @@
     2.4  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
     2.5  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
     2.6  val t = TermC.str2term "sqrt 4";
     2.7 +Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t;
     2.8  
     2.9 -(* error-from-Skip_Proof.make_thm: inherited errors are marked TOODOO.1 in test/*
    2.10 - exception TYPE raised (line 169 of "consts.ML"): Illegal type
    2.11 -   for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
    2.12 -      Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t
    2.13 -( **)
    2.14  "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
    2.15    ((ThyC.get_theory "Isac_Knowledge"),
    2.16      ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);