1.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri Sep 03 17:19:20 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Mon Sep 06 14:48:38 2010 +0200
     1.3 @@ -91,10 +91,24 @@
     1.4  
     1.5  (*13.9.02--------------
     1.6  type ctr = (loc * pos) list;
     1.7 -val ops = [("PLUS","op +"),("minus","op -"),("TIMES","op *"),
     1.8 +val ops = [("PLUS","op +"),("MINUS","op -"),("TIMES","op *"),
     1.9  	   ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")];
    1.10 +ML {* 
    1.11 +@{term "PLUS"};   (*Free ("PLUS", "'a") : term*)
    1.12 +@{term "plus"};   (*Const ("Groups.plus_class.plus", "'a => 'a => 'a")*)
    1.13 +@{term "MINUS"};  (*Free ("MINUS", "'a")*)
    1.14 +@{term "minus"};  (*Const ("Groups.minus_class.minus", "'a => 'a => 'a")*)
    1.15 +@{term "TIMES"};  (*Free ("TIMES", "'a")*)
    1.16 +@{term "times"};  (*Const ("Groups.times_class.times", "'a => 'a => 'a")*)
    1.17 +@{term "CANCEL"}; (*Free ("CANCEL", "'a")*)
    1.18 +@{term "cancel"}; (*Free ("cancel", "'a")*)
    1.19 +@{term "POWER"};  (*Free ("POWER", "'a")*)
    1.20 +@{term "pow"};    (*Free ("pow", "'a")*)
    1.21 +@{term "SQRT"};   (*Free ("SQRT", "'a")*)
    1.22 +@{term "sqrt"};   (*Const ("NthRoot.sqrt", "RealDef.real => RealDef.real")*)
    1.23 +*}
    1.24  fun op_intern op_ =
    1.25 -  case assoc (ops,op_) of
    1.26 +  case assoc (ops, op_) of
    1.27      SOME op' => op' | NONE => raise error ("op_intern: no op= "^op_);
    1.28  -----------------------*)
    1.29