test/Tools/isac/ProgLang/calculate-float.sml
branchisac-update-Isa09-2
changeset 38014 3e11e3c2dc42
parent 37960 ec20007095f2
     1.1 --- a/test/Tools/isac/ProgLang/calculate-float.sml	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/calculate-float.sml	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  val thy = Float.thy;
     1.5  
     1.6  (*.calculate the value of a pair of floats.*)
     1.7 -val ((a,b),(c,d)) = calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
     1.8 +val ((a,b),(c,d)) = calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
     1.9  
    1.10  
    1.11  (*.build the term.*)
    1.12 @@ -113,7 +113,7 @@
    1.13  
    1.14  (*.the function evaluating a binary operator.*)
    1.15  val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
    1.16 -val SOME (thmid, t) = eval_binop "#add_" "op +" t thy;
    1.17 +val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" t thy;
    1.18  term2str t;
    1.19  
    1.20