1.1 --- a/src/Tools/isac/ProgLang/evaluate.sml	Sun Jul 18 18:30:09 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml	Sun Jul 18 21:15:21 2021 +0200
     1.3 @@ -291,25 +291,6 @@
     1.4  > t = var_op_float v \<^const_name>\<open>plus\<close> optype HOLogic.realT ((11,~1),(0,0));
     1.5  val it = true : bool*)
     1.6  
     1.7 -(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
     1.8 -(** )
     1.9 -fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
    1.10 -    TermC.mk_num_op_var v op_ optype ntyp v1
    1.11 -  | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
    1.12 -    let val pT = TermC.pairT T T
    1.13 -    in Const (op_, optype) $ 
    1.14 -	     (Const ("Float.Float", (TermC.pairT pT pT) --> T)
    1.15 -		    $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
    1.16 -				    (Free (TermC.str_of_int v2, T)))
    1.17 -			     (TermC.pairt (Free (TermC.str_of_int p1, T))
    1.18 -				    (Free (TermC.str_of_int p2, T))))) $ v
    1.19 -    end;
    1.20 -(*> val t = str2term "a + b";
    1.21 -> val Const (\<^const_name>\<open>plus\<close>, optype) $ _ $ _ = t;
    1.22 -> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
    1.23 -> t = float_op_var v \<^const_name>\<open>plus\<close> optype HOLogic.realT ((11,~1),(0,0));
    1.24 -val it = true : bool*)
    1.25 -
    1.26  end
    1.27  
    1.28