src/Tools/isac/Knowledge/Delete.thy
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 38014 3e11e3c2dc42
child 38034 928cebc9c4aa
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba
    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))
    34   | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = 
    34   | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = 
    35     raise error ("calc: not impl. for Float (("^
    35     error ("calc: not impl. for Float (("^
    36 		 (string_of_int a  )^","^(string_of_int b  )^"), ("^
    36 		 (string_of_int a  )^","^(string_of_int b  )^"), ("^
    37 		 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
    37 		 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
    38 		 (string_of_int c  )^","^(string_of_int d  )^"), ("^
    38 		 (string_of_int c  )^","^(string_of_int d  )^"), ("^
    39 		 (string_of_int p21)^","^(string_of_int p22)^"))");
    39 		 (string_of_int p21)^","^(string_of_int p22)^"))");
    40 (*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0)); 
    40 (*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));