src/Tools/isac/Knowledge/Delete.thy
branchisac-update-Isa09-2
changeset 38034 928cebc9c4aa
parent 38031 460c24a6a6ba
child 38036 02a9b2540eb7
equal deleted inserted replaced
38033:491b133d154a 38034:928cebc9c4aa
    23     if b < d 
    23     if b < d 
    24     then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
    24     then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
    25     else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
    25     else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
    26   | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)
    26   | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)
    27     ((a - c,0),(0,0))
    27     ((a - c,0),(0,0))
    28   | calc "op *" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)
    28   | calc "Groups.times_class.times" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)
    29     ((a * c, b + d), (0, 0))
    29     ((a * c, b + d), (0, 0))
    30   | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
    30   | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
    31     ((a div c, 0), (0, 0))
    31     ((a div c, 0), (0, 0))
    32   | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
    32   | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
    33     ((power a c, 0), (0, 0))
    33     ((power a c, 0), (0, 0))