src/Tools/isac/Knowledge/Delete.thy
branchisac-update-Isa09-2
changeset 38034 928cebc9c4aa
parent 38031 460c24a6a6ba
child 38036 02a9b2540eb7
     1.1 --- a/src/Tools/isac/Knowledge/Delete.thy	Tue Sep 28 10:01:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Delete.thy	Tue Sep 28 10:10:26 2010 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4      else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
     1.5    | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)
     1.6      ((a - c,0),(0,0))
     1.7 -  | calc "op *" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)
     1.8 +  | calc "Groups.times_class.times" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)
     1.9      ((a * c, b + d), (0, 0))
    1.10    | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
    1.11      ((a div c, 0), (0, 0))