1.1 --- a/src/Tools/isac/ProgLang/calculate.sml	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/calculate.sml	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -137,22 +137,22 @@
     1.4      end;
     1.5   (*
     1.6  >  val t = (term_of o the o (parse thy)) "#3 + #4";
     1.7 ->  val eval_fn = the (assoc (!eval_list, "op +"));
     1.8 ->  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
     1.9 +>  val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
    1.10 +>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
    1.11  >  Syntax.string_of_term (thy2ctxt thy) t';
    1.12  >  atomty t';
    1.13  > 
    1.14  >  val t = (term_of o the o (parse thy)) "(a + #3) + #4";
    1.15 ->  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
    1.16 +>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
    1.17  >  Syntax.string_of_term (thy2ctxt thy) t';
    1.18  > 
    1.19  >  val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
    1.20 ->  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
    1.21 +>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
    1.22  >  Syntax.string_of_term (thy2ctxt thy) t';
    1.23  > 
    1.24  >  val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
    1.25  >  atomty t;
    1.26 ->  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
    1.27 +>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
    1.28  >  Syntax.string_of_term (thy2ctxt thy) t';
    1.29  >  val it = "#3 + (#4 + a) = #7 + a" : string
    1.30  >
    1.31 @@ -273,15 +273,15 @@
    1.32  -------------------------------------------------------------------6.8.02:
    1.33  
    1.34  > val ct = (the o (parse thy)) "a+#3+#4";
    1.35 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
    1.36 +> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
    1.37  val it = SOME ("add_3_4","a + 3 + 4 = a + 7  [a + 3 + 4 = a + 7]")
    1.38   
    1.39  > val ct = (the o (parse thy)) "#3+(#4+a)";
    1.40 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
    1.41 +> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
    1.42  val it = SOME ("add_3_4","3 + (4 + a) = 7 + a  [3 + (4 + a) = 7 + a]")
    1.43   
    1.44  > val ct = (the o (parse thy)) "a+(#3+#4)+#5";
    1.45 -> get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct;
    1.46 +> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
    1.47  val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option
    1.48  
    1.49  > val ct = (the o (parse thy)) "#3*(#4*a)";