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))