1.1 --- a/src/Tools/isac/Knowledge/Delete.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Delete.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -19,15 +19,15 @@
     1.4  
     1.5  (*.used for calculating built in binary operations in Isabelle2002.
     1.6     integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)
     1.7 -fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int)  = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
     1.8 +fun calc "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int)  = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
     1.9      if b < d 
    1.10      then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
    1.11      else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
    1.12 -  | calc "op -" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)
    1.13 +  | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)
    1.14      ((a - c,0),(0,0))
    1.15    | calc "op *" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)
    1.16      ((a * c, b + d), (0, 0))
    1.17 -  | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
    1.18 +  | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
    1.19      ((a div c, 0), (0, 0))
    1.20    | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
    1.21      ((power a c, 0), (0, 0))
    1.22 @@ -37,7 +37,7 @@
    1.23  		 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
    1.24  		 (string_of_int c  )^","^(string_of_int d  )^"), ("^
    1.25  		 (string_of_int p21)^","^(string_of_int p22)^"))");
    1.26 -(*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0)); 
    1.27 +(*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0)); 
    1.28  val it = ((1,0),(0,0))*)
    1.29  
    1.30  (*.convert internal floatingpoint prepresentation to int and float.*)
    1.31 @@ -76,9 +76,9 @@
    1.32  				    (Free (str_of_int p2, T)))))
    1.33      end;
    1.34  (*> val t = str2term "a + b";
    1.35 -> val Const ("op +", optype) $ _ $ _ = t;
    1.36 +> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
    1.37  > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
    1.38 -> t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0));
    1.39 +> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
    1.40  val it = true : bool*)
    1.41  
    1.42  (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
    1.43 @@ -94,9 +94,9 @@
    1.44  				    (Free (str_of_int p2, T))))) $ v
    1.45      end;
    1.46  (*> val t = str2term "a + b";
    1.47 -> val Const ("op +", optype) $ _ $ _ = t;
    1.48 +> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
    1.49  > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
    1.50 -> t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0));
    1.51 +> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
    1.52  val it = true : bool*)
    1.53  *}
    1.54